NYLL
Module

Exists_dlog_of_cartierOperator_fixed.lean

Nyll.AlgebraicCurves.Differentials.Exists_dlog_of_cartierOperator_fixed
27 declarations indexed from sourceView source ↗

Module documentation

Exists dlog of cartier Operator fixed

Imports5
Imported by2

Declarations

lemma

span_D_eq_top

L38 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.span_D_eq_top
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma span_D_eq_top (t : F) (hdt : D K F t ≠ 0) :
    Submodule.span F {D K F t} = ⊤
lemma

exists_coeff

L43 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.exists_coeff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma exists_coeff (t : F) (hdt : D K F t ≠ 0) (ω : Ω[F⁄K]) :
    ∃ c : F, ω = c • D K F t
lemma

coeff_unique

L50 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.coeff_unique
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
omit [AlgebraicCurve.IsCurveOver K F] in
Lean source · statement
lemma coeff_unique (t : F) (hdt : D K F t ≠ 0) {c₁ c₂ : F}
    (h : c₁ • D K F t = c₂ • D K F t) : c₁ = c₂
def

dcoord

L57 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
def dcoord (t : F) (hdt : D K F t ≠ 0) (f : F) : F
lemma

dcoord_spec

L60 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_spec
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma dcoord_spec (t : F) (hdt : D K F t ≠ 0) (f : F) :
    D K F f = dcoord t hdt f • D K F t
lemma

dcoord_self

L64 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_self
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma dcoord_self (t : F) (hdt : D K F t ≠ 0) : dcoord t hdt t = 1
lemma

dcoord_add

L67 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_add
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma dcoord_add (t : F) (hdt : D K F t ≠ 0) (f g : F) :
    dcoord t hdt (f + g) = dcoord t hdt f + dcoord t hdt g
lemma

dcoord_smul

L72 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma dcoord_smul (t : F) (hdt : D K F t ≠ 0) (k : K) (f : F) :
    dcoord t hdt (k • f) = k • dcoord t hdt f
lemma

dcoord_leibniz

L77 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_leibniz
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma dcoord_leibniz (t : F) (hdt : D K F t ≠ 0) (f g : F) :
    dcoord t hdt (f * g) = f * dcoord t hdt g + g * dcoord t hdt f
def

dcoordD

L83 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoordD
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
def dcoordD (t : F) (hdt : D K F t ≠ 0) : Derivation K F F
lemma

dcoordD_apply

L96 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoordD_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section coord
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma dcoordD_apply (t : F) (hdt : D K F t ≠ 0) (f : F) :
    dcoordD t hdt f = dcoord t hdt f
lemma

dtlc_app

L105 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dtlc_app
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [CharP F p] in
Lean source · statement
lemma dtlc_app (t : F) (hdt : D K F t ≠ 0) (f : F) :
    (dcoordD (K := K) t hdt).toLinearMap f = dcoordD (K := K) t hdt f
lemma

endo_mul_app

L108 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.endo_mul_app
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [CharP F p] [AlgebraicCurve.IsCurveOver K F] in
Lean source · statement
lemma endo_mul_app (f g : F →ₗ[K] F) (x : F) : (f * g) x = f (g x)
lemma

dcoord_frob

L110 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_frob
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [Fact p.Prime] in
Lean source · statement
lemma dcoord_frob (t : F) (hdt : D K F t ≠ 0) (c : F) :
    dcoordD (K := K) t hdt (c ^ p) = 0
lemma

dcoord_t_pow

L114 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_t_pow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [CharP F p] in
Lean source · statement
lemma dcoord_t_pow (t : F) (hdt : D K F t ≠ 0) (i : ℕ) :
    dcoordD (K := K) t hdt (t ^ i) = i • t ^ (i - 1)
lemma

dcoord_digit

L119 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_digit
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [Fact p.Prime] in
Lean source · statement
lemma dcoord_digit (t : F) (hdt : D K F t ≠ 0) (c : F) (i : ℕ) :
    dcoordD (K := K) t hdt (c ^ p * t ^ i) = i • (c ^ p * t ^ (i - 1))
lemma

dcoord_iter_digit

L124 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_iter_digit
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [Fact p.Prime] in
Lean source · statement
lemma dcoord_iter_digit (t : F) (hdt : D K F t ≠ 0) (c : F) (i k : ℕ) :
    ((dcoordD (K := K) t hdt).toLinearMap ^ k) (c ^ p * t ^ i)
      = i.descFactorial k • (c ^ p * t ^ (i - k))
lemma

dcoord_iter_sum

L137 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_iter_sum
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma dcoord_iter_sum (t : F) (hdt : D K F t ≠ 0) (a : Fin p → F) :
    ((dcoordD (K := K) t hdt).toLinearMap ^ (p - 1)) (∑ i : Fin p, a i ^ p * t ^ (i : ℕ))
      = (p - 1).factorial • a ⟨p - 1, Nat.sub_lt (Fact.out : p.Prime).pos one_pos⟩ ^ p
lemma

dcoord_iter_p_sum

L155 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.dcoord_iter_p_sum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [Fact p.Prime] in
Lean source · statement
lemma dcoord_iter_p_sum (t : F) (hdt : D K F t ≠ 0) (a : Fin p → F) :
    ((dcoordD (K := K) t hdt).toLinearMap ^ p) (∑ i : Fin p, a i ^ p * t ^ (i : ℕ)) = 0
lemma

factorial_cast_eq_neg_one

L162 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.factorial_cast_eq_neg_one
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section digits
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
lemma factorial_cast_eq_neg_one : (((p - 1).factorial : ℕ) : F) = -1
lemma

D_natCast

L175 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.D_natCast
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section cartier
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [CharP F p] [AlgebraicCurve.IsCurveOver K F] in
Lean source · statement
lemma D_natCast (n : ℕ) : D K F (n : F) = 0
lemma

natCast_ne_zero_of_lt

L180 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.natCast_ne_zero_of_lt
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section cartier
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [AlgebraicCurve.IsCurveOver K F] in
Lean source · statement
lemma natCast_ne_zero_of_lt (i : ℕ) (hip : 0 < i) (hlt : i < p) : ((i : ℕ) : F) ≠ 0
lemma

smul_D_exact

L191 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.smul_D_exact
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section cartier
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [CharP F p] [AlgebraicCurve.IsCurveOver K F] in
Lean source · statement
lemma smul_D_exact (t : F) (i : ℕ) (hν : ((i + 1 : ℕ) : F) ≠ 0) :
    (t ^ i : F) • D K F t = D K F (((i + 1 : ℕ) : F)⁻¹ * t ^ (i + 1))
lemma

cartier_coord

L200 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.cartier_coord
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section cartier
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [AlgebraicCurve.IsCurveOver K F] in
Lean source · statement
lemma cartier_coord (t : F) (_hdt : D K F t ≠ 0) (C : Ω[F⁄K] →+ Ω[F⁄K])
    (hsemi : ∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω)
    (hker : ∀ f : F, C (D K F f) = 0)
    (hlog : ∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f)
    (a : Fin p → F) :
    C ((∑ i : Fin p, a i ^ p * t ^ (i : ℕ)) • D K F t)
      = a ⟨p - 1, Nat.sub_lt (Fact.out : p.Prime).pos one_pos⟩ • D K F t
lemma

exists_ker_of_pow_eq_zero

L229 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.exists_ker_of_pow_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section cartier
variable (p : ℕ) [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F]
omit [Fact p.Prime] [CharP F p] [AlgebraicCurve.IsCurveOver K F] in
Lean source · statement
lemma exists_ker_of_pow_eq_zero (τ : F →ₗ[K] F) (hτp : τ ^ p = 0) :
    ∃ h : F, h ≠ 0 ∧ τ h = 0
theorem

fixed_is_dlog_main

L249 ↗
AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed.Star2C.fixed_is_dlog_main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
namespace Star2C
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section main
variable [AlgebraicCurve.IsCurveOver K F]
Lean source · statement
theorem fixed_is_dlog_main (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectField K]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (hb : ∀ (d : Derivation K F F) (a : F),
        (d.toLinearMap + LinearMap.mulLeft K a) ^ p
          = d.toLinearMap ^ p + LinearMap.mulLeft K (a ^ p + (d.toLinearMap ^ (p - 1)) a))
    (C : Ω[F⁄K] →+ Ω[F⁄K])
    (hsemi : ∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω)
    (hker : ∀ f : F, C (KaehlerDifferential.D K F f) = 0)
    (hlog : ∀ f : F, C (f ^ (p - 1) • KaehlerDifferential.D K F f) = KaehlerDifferential.D K F f)
    (w : Ω[F⁄K]) (hfix : C w = w) :
    ∃ h : F, h ≠ 0 ∧ w = h⁻¹ • KaehlerDifferential.D K F h
theorem

exists_dlog_of_cartierOperator_fixed

L317 ↗
AlgebraicCurve.exists_dlog_of_cartierOperator_fixed
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_dlog_of_cartierOperator_fixed
universe u v
open KaehlerDifferential
Lean source · statement
theorem _root_.AlgebraicCurve.exists_dlog_of_cartierOperator_fixed {K : Type u} {F : Type v}
    [Field K] [Field F] [Algebra K F] [AlgebraicCurve.IsCurveOver K F] (p : ℕ)
    [Fact p.Prime] [CharP K p] [PerfectField K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (C : Ω[F⁄K] →+ Ω[F⁄K])
    (hsemi : ∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω)
    (hker : ∀ f : F, C (KaehlerDifferential.D K F f) = 0)
    (hlog : ∀ f : F, C (f ^ (p - 1) • KaehlerDifferential.D K F f) = KaehlerDifferential.D K F f)
    (w : Ω[F⁄K]) (hfix : C w = w) :
    ∃ h : F, h ≠ 0 ∧ w = h⁻¹ • KaehlerDifferential.D K F h

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