NYLL
Module

PDigits_existsUnique.lean

Nyll.AlgebraicCurves.Places.PDigits_existsUnique
4 declarations indexed from sourceView source ↗

Module documentation

PDigits exists Unique

Imports6
Imported by5

Declarations

theorem

transcendental_of_D_ne_zero'

L38 ↗
AlgebraicCurves.Places.Proofs.PDigits_existsUnique.AlgebraicCurve.transcendental_of_D_ne_zero'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PDigits_existsUnique
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem transcendental_of_D_ne_zero' [PerfectField K] {t : F}
    (hdt : D K F t ≠ 0) : Transcendental K t
theorem

pow_ne_of_D_ne_zero'

L57 ↗
AlgebraicCurves.Places.Proofs.PDigits_existsUnique.AlgebraicCurve.pow_ne_of_D_ne_zero'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PDigits_existsUnique
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem pow_ne_of_D_ne_zero' (p : ℕ) [Fact p.Prime] [CharP K p] {t : F}
    (hdt : D K F t ≠ 0) (a : F) : a ^ p ≠ t
theorem

pDigits_existsUnique_impl

L64 ↗
AlgebraicCurves.Places.Proofs.PDigits_existsUnique.AlgebraicCurve.pDigits_existsUnique_impl
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PDigits_existsUnique
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem pDigits_existsUnique_impl [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 : D K F t ≠ 0) (g : F) :
    ∃! a : Fin p → F, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)
theorem

pDigits_existsUnique

L76 ↗
AlgebraicCurve.pDigits_existsUnique
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PDigits_existsUnique
universe u v
open KaehlerDifferential
Lean source · statement
theorem _root_.AlgebraicCurve.pDigits_existsUnique {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]
    {t : F} (hdt : D K F t ≠ 0) (g : F) :
    ∃! a : Fin p → F, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)

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