AlgebraicCurve.existsUnique_pDigits_of_D_ne_zero
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.ExistsUnique_pDigits_of_D_ne_zeroLean source · statement
theorem _root_.AlgebraicCurve.existsUnique_pDigits_of_D_ne_zero {K : Type*} {F : Type*} [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]
{t : F} (hdt : KaehlerDifferential.D K F t ≠ 0) (g : F) :
∃! a : Fin p → F, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)