NYLL
Module

CartierB_linearIndependent_of_cartier_fixed.lean

Nyll.AlgebraicCurves.Differentials.Cartier.CartierB_linearIndependent_of_cartier_fixed
2 declarations indexed from sourceView source ↗

Module documentation

Cartier B linear Independent of cartier fixed

Imports4
Imported by2

Declarations

theorem

exists_natCast_eq_of_pow_char_eq

L28 ↗
AlgebraicCurves.Differentials.Cartier.Proofs.CartierB_linearIndependent_of_cartier_fixed.exists_natCast_eq_of_pow_char_eq
Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Differentials.Cartier.Proofs.CartierB_linearIndependent_of_cartier_fixed
noncomputable section
Lean source · statement
theorem exists_natCast_eq_of_pow_char_eq {K : Type*} [Field K] (p : ℕ)
    [Fact p.Prime] [CharP K p] {x : K} (hx : x ^ p = x) : ∃ m : ℕ, (m : K) = x
theorem

linearIndependent_of_cartier_fixed

L77 ↗
AlgebraicCurve.CartierB.linearIndependent_of_cartier_fixed
Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Differentials.Cartier.Proofs.CartierB_linearIndependent_of_cartier_fixed
noncomputable section
Lean source · statement
theorem _root_.AlgebraicCurve.CartierB.linearIndependent_of_cartier_fixed {K F : Type*} [Field K]
    [Field F] [Algebra K F] [AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime]
    [CharP K p] [PerfectField K] (C : Ω[F⁄K] →+ Ω[F⁄K])
    (hsemi : ∀ (f : F) (η : Ω[F⁄K]), C (f ^ p • η) = f • C η)
    {n : ℕ} {w : Fin n → Ω[F⁄K]} (hfix : ∀ i, C (w i) = w i)
    (hFp : ∀ c : Fin n → ℕ, ∑ i, c i • w i = 0 → ∀ i, p ∣ c i) :
    LinearIndependent K w

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.