TateParameter.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

23 declarations, 0 contain sorry, 0 declared as axioms

The Tate parameter power series

Let k be a field complete with respect to a rank 1 nonarchimedean valuation. The j-invariant of the Tate curve E_q is j(q) = q⁻¹ + 744 + 196884q + ⋯, and Silverman, Advanced topics in the arithmetic of elliptic curves, Lemma V.5.2, states that q ↦ j(q) is a bijection from {q : 0 < |q| < 1} onto {j : |j| > 1}, whose inverse is given by a power series q = j⁻¹ + 744j⁻² + 750420j⁻³ + ⋯ ∈ ℤ⟦j⁻¹⟧ with integer coefficients. This file constructs that inverse map WeierstrassCurve.tateParameter, as honest data (no appeal to choice), in three steps.

Step 1: the formal series `1/j ∈ ℤ⟦q⟧` (`TateCurve.jInv`)

j(q) itself is not a power series (it has the pole q⁻¹), but its reciprocal is: 1/j = Δ(q)/c₄(q)³ where Δ(q) = q∏_{n≥1}(1 - qⁿ)²⁴ and c₄(q) = 1 + 240∑σ₃(n)qⁿ, both in ℤ⟦q⟧. The infinite product is a tprod in the X-adic topology on ℤ⟦X⟧ (each coefficient is a finite computation, PowerSeries.WithPiTopology), and c₄³ has constant coefficient 1, so it is invertible over ℤ (PowerSeries.invOfUnit — no denominators appear). The result is jInv = q - 744q² + 356652q³ - ⋯, with jInv(0) = 0 and linear coefficient 1.

Step 2: formal compositional inversion (`TateCurve.jInvReverse`)

A power series f = u·X + a₂X² + ⋯ with zero constant term and invertible linear coefficient has a unique compositional inverse g with g(f) = f(g) = X, with coefficients in the same ring. Mathlib provides this as PowerSeries.substInv (with the composition identities subst_substInv_right and subst_substInv_left), constructed by the coefficient recursion bₙ₊₁ = -⅟u·[Xⁿ⁺¹](f ∘ (∑_{i ≤ n} bᵢXⁱ)). Note that the only division ever performed is by the linear coefficient u — which for jInv is 1 — and not by n, as the closed Lagrange inversion formula bₙ = (1/n)·[Xⁿ⁻¹](X/f)ⁿ would require; division by n would be illegal in the intended targets of the coefficients (k may be 𝔽_q((t)), where char k ∣ n happens). Integrality of the coefficients of the inverse j-series — which Silverman remarks on in V.5.2 — is thereby true by construction.

TateCurve.jInvReverse := substInv jInv = X + 744X² + 750420X³ + ⋯ is the series we are after.

Step 3: evaluation (`WeierstrassCurve.tateParameter`)

Finally tateParameter j := ∑_{n≥1} bₙ (j⁻¹)ⁿ, a tsum in k. For |j| > 1 the terms have norm at most |j⁻¹|ⁿ → 0 (nonarchimedean bound: the coefficients are integers!), so the series converges by completeness of k; for |j| ≤ 1 the tsum takes junk values, consistently with the other series in Tate's theory (tateA₄, tateA₆, …). Only a field and a topology are needed to state the definition, so it applies verbatim in the rank 1 generality (ℂ_p, completed maximal unramified extensions, …).

The interaction with the valuation — for |j| > 1 the series converges with valuation exactly |j|⁻¹, so tateParameter j lies in the punctured open unit disc — is proved in FLT.KnownIn1980s.EllipticCurves.TateCurve (WeierstrassCurve.valuation_tateParameter_eq), where the Tate parameter WeierstrassCurve.q of an elliptic curve is defined. The characterising properties — j(tateParameter j) = j for |j| > 1 and tateParameter (j(q)) = q for 0 < |q| < 1 (the two halves of Silverman V.5.2) — are future work there: their proofs will combine the formal identity subst_jInvReverse of Step 2 with the usual formal-to-convergent bridge (evaluation of a formal subst identity at a point where all the series converge).

Because the coefficients are universal integers, tateParameter commutes with every continuous morphism of topological fields; this is what makes the Tate parameter functorial (WeierstrassCurve.q_baseChange) with no uniqueness argument at the level of k.

Imports (10)

Imported by 3 files

def TateCurve.sInt The formal series sₖ(q) = ∑_{n≥1} σₖ(n)qⁿ ∈ ℤ⟦q⟧ (integer-coefficient version of TateCurve.s; recall σₖ(0) = 0) line 99 source
Source documentation
The formal series sₖ(q) = ∑_{n≥1} σₖ(n)qⁿ ∈ ℤ⟦q⟧ (integer-coefficient version of TateCurve.s; recall σₖ(0) = 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int
Proof uses: PowerSeries.mk, ArithmeticFunction, ArithmeticFunction.sigma
6 instances, coercions and auxiliary constants left out.
```
noncomputable def sInt (k : ℕ) : ℤ⟦X⟧ := .mk fun n ↦ (σ k n : ℤ)
```
Mentions: TateCurve.X
def TateCurve.c₄Formal The formal c₄-series c₄(q) = 1 + 240s₃(q) = 1 + 240q + 2160q² + ⋯ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the Eisenstein series E₄ line 103 source
Source documentation
The formal c₄-series c₄(q) = 1 + 240s₃(q) = 1 + 240q + 2160q² + ⋯ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the Eisenstein series E₄.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: HAdd.hAdd, Unit, OfNat.ofNat, HMul.hMul, TateCurve.sInt, Nat
14 instances, coercions and auxiliary constants left out.
```
noncomputable def c₄Formal : ℤ⟦X⟧ := 1 + 240 * sInt 3
```
Mentions: TateCurve.X, TateCurve.sInt
def TateCurve.ΔFormal The formal discriminant Δ(q) = q∏_{n≥1}(1 - qⁿ)²⁴ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the modular discriminant, ∑ τ(n)qⁿ with τ Ramanujan's tau line 109 source
Source documentation
The formal discriminant Δ(q) = q∏_{n≥1}(1 - qⁿ)²⁴ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the modular discriminant, ∑ τ(n)qⁿ with τ Ramanujan's tau. The product is a tprod in the X-adic topology, multipliable by PowerSeries.WithPiTopology.multipliable_one_sub_X_pow.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: HMul.hMul, Unit, PowerSeries.X, HPow.hPow, Nat, tprod, HSub.hSub, OfNat.ofNat, HAdd.hAdd, SummationFilter.unconditional
23 instances, coercions and auxiliary constants left out.
```
noncomputable def ΔFormal : ℤ⟦X⟧ := X * (∏' n : ℕ, (1 - X ^ (n + 1))) ^ 24
```
Mentions: TateCurve.X
def TateCurve.jInv The formal series 1/j = Δ(q)/c₄(q)³ = q - 744q² + 356652q³ - ⋯ ∈ ℤ⟦q⟧: the reciprocal of the j-invariant of the Tate curve line 115 source
Source documentation
The formal series 1/j = Δ(q)/c₄(q)³ = q - 744q² + 356652q³ - ⋯ ∈ ℤ⟦q⟧: the reciprocal of the j-invariant of the Tate curve. Since c₄³ has constant coefficient 1 its inverse PowerSeries.invOfUnit (c₄Formal ^ 3) 1 has integer coefficients: no denominators are introduced.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: HMul.hMul, Unit, TateCurve.ΔFormal, PowerSeries.invOfUnit, HPow.hPow, Nat, TateCurve.c₄Formal, OfNat.ofNat, Units
13 instances, coercions and auxiliary constants left out.
```
noncomputable def jInv : ℤ⟦X⟧ := ΔFormal * invOfUnit (c₄Formal ^ 3) 1
…
```
Mentions: TateCurve.X, TateCurve.ΔFormal, TateCurve.c₄Formal
theorem TateCurve.constantCoeff_jInv line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, RingHom, PowerSeries, Unit, PowerSeries.constantCoeff, TateCurve.jInv, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HMul.hMul, PowerSeries.X, HPow.hPow, Nat, tprod, HSub.hSub, HAdd.hAdd, SummationFilter.unconditional, PowerSeries.invOfUnit, TateCurve.c₄Formal, Units, map_mul, congr, PowerSeries.constantCoeff_X, map_pow and 6 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem TateCurve.coeff_one_jInv line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, OfNat.ofNat, Nat, TateCurve.jInv
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HMul.hMul, HPow.hPow, tprod, HSub.hSub, PowerSeries.X, HAdd.hAdd, SummationFilter.unconditional, PowerSeries.invOfUnit, TateCurve.c₄Formal, Units, mul_assoc, PowerSeries.coeff_succ_X_mul, RingHom, PowerSeries.constantCoeff, congrFun and 26 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance TateCurve.(instance at line 130) line 130 source
Source documentation
The linear coefficient of jInv is (invertibly) 1: the hypothesis under which mathlib's compositional inversion PowerSeries.substInv applies.
```
noncomputable instance : Invertible (coeff 1 jInv) := invertibleOne.copy _ coeff_one_jInv
```
Mentions: TateCurve.jInv, TateCurve.coeff_one_jInv
def TateCurve.jInvReverse Documented declaration: jInvReverse line 137 source
Source documentation
The formal inverse j-series ψ = X + 744X² + 750420X³ + 872769632X⁴ + ⋯ ∈ ℤ⟦X⟧: the compositional inverse PowerSeries.substInv of jInv, so that formally q = ψ(1/j) (Silverman, ATAEC V.5.2 — the integrality of the coefficients is by construction, see the module docstring).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: PowerSeries.substInv, TateCurve.jInv
2 instances, coercions and auxiliary constants left out.
```
noncomputable def jInvReverse : ℤ⟦X⟧ := substInv jInv
```
Mentions: TateCurve.X, TateCurve.jInv
theorem TateCurve.subst_jInvReverse The defining property of jInvReverse: ψ(jInv(q)) = q as formal power series line 141 source
Source documentation
The defining property of jInvReverse: ψ(jInv(q)) = q as formal power series. This is the identity from which both halves of Silverman V.5.2 follow by evaluation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, MvPowerSeries, Unit, Int, PowerSeries.subst, TateCurve.jInv, TateCurve.jInvReverse, PowerSeries.X
Proof uses: PowerSeries.subst_substInv_left, TateCurve.constantCoeff_jInv
6 instances, coercions and auxiliary constants left out.
```
theorem subst_jInvReverse : PowerSeries.subst jInv jInvReverse = X :=
…
```
Mentions: TateCurve.jInv, TateCurve.jInvReverse, TateCurve.X
theorem TateCurve.jInv_subst_jInvReverse The composition in the other order: jInv(ψ(w)) = w as formal power series line 145 source
Source documentation
The composition in the other order: jInv(ψ(w)) = w as formal power series.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, MvPowerSeries, Unit, Int, PowerSeries.subst, TateCurve.jInvReverse, TateCurve.jInv, PowerSeries.X
Proof uses: PowerSeries.subst_substInv_right, TateCurve.constantCoeff_jInv
6 instances, coercions and auxiliary constants left out.
```
theorem jInv_subst_jInvReverse : PowerSeries.subst jInvReverse jInv = X :=
…
```
Mentions: TateCurve.jInvReverse, TateCurve.jInv, TateCurve.X
theorem TateCurve.constantCoeff_jInvReverse line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, RingHom, PowerSeries, Unit, PowerSeries.constantCoeff, TateCurve.jInvReverse, OfNat.ofNat
Proof uses: PowerSeries.constantCoeff_substInv, TateCurve.jInv
8 instances, coercions and auxiliary constants left out.
theorem TateCurve.coeff_one_jInvReverse line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, OfNat.ofNat, Nat, TateCurve.jInvReverse
Proof uses: Eq.mpr, Invertible.invOf, TateCurve.jInv, id, congrFun', congrArg, PowerSeries.coeff_one_substInv, invOf_eq_right_inv, HMul.hMul, TateCurve.coeff_one_jInv, mul_one, Eq.refl
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def TateCurve.evalInt The evaluation ∑ₙ Fₙqⁿ ∈ k of an integral power series F ∈ ℤ⟦X⟧ at a point q of a topological field (junk value if the series does not converge) line 171 source
Source documentation
The evaluation ∑ₙ Fₙqⁿ ∈ k of an integral power series F ∈ ℤ⟦X⟧ at a point q of a topological field (junk value if the series does not converge).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, PowerSeries, Int
Proof uses: tsum, Nat, HMul.hMul, LinearMap, RingHom.id, Unit, PowerSeries.coeff, HPow.hPow, SummationFilter.unconditional
23 instances, coercions and auxiliary constants left out.
```
noncomputable def evalInt (q : k) (F : ℤ⟦X⟧) : k := ∑' n : ℕ, ((coeff n F : ℤ) : k) * q ^ n
…
```
Mentions: TateCurve.X
theorem TateCurve.evalInt_X line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, Eq, TateCurve.evalInt, PowerSeries.X, Int
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, tsum, Nat, HMul.hMul, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, HPow.hPow, SummationFilter.unconditional, OfNat.ofNat, ite, SummationFilter, optParam, funext and 13 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem TateCurve.evalInt_add line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, IsTopologicalRing, T2Space, PowerSeries, Int, Summable, Nat, HMul.hMul, LinearMap, RingHom.id, Unit, PowerSeries.coeff, HPow.hPow, SummationFilter.unconditional, Eq, TateCurve.evalInt, HAdd.hAdd
Proof uses: Eq.mpr, tsum, id, congrFun', congrArg, SummationFilter, optParam, funext, Eq.trans, map_add, Int.cast_add, add_mul, Summable.tsum_add
73 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem TateCurve.summable_of_valuation_le_pow Documented declaration: summable_of_valuation_le_pow line 196 source
Source documentation
The convergence criterion for series over a nonarchimedean local field: if each term of f is bounded by |q|^(e i) for an exponent function e with finite sublevel sets, then f is summable — its terms tend to zero cofinitely, which suffices by completeness and the nonarchimedean property (no absolute convergence is needed — contrast the archimedean case).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, ValuativeRel, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Nat, Set.Finite, Set.ofPred, LE.le, HPow.hPow, Summable, SummationFilter.unconditional
Proof uses: UniformSpace, IsTopologicalAddGroup.rightUniformSpace, IsUniformAddGroup, isUniformAddGroup_of_addCommGroup, NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero, Eq.mpr, Filter.Tendsto, Filter.cofinite, nhds, Units, True, Filter.Eventually, Membership.mem, Set, HSub.hSub, id, Eq, congrArg, propext, Filter.HasBasis.tendsto_right_iff and 15 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem summable_of_valuation_le_pow {ι : Type*} {q : k} (hq : valuation k q < 1)
    {f : ι → k} (e : ι → ℕ) (he : ∀ N, {i | e i < N}.Finite)
    (hf : ∀ i, valuation k (f i) ≤ valuation k q ^ e i) : Summable f := by
…
```
theorem TateCurve.tendsto_pow_nhds_zero Powers of an element of the open unit disc tend to zero line 214 source
Source documentation
Powers of an element of the open unit disc tend to zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, ValuativeRel, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Filter.Tendsto, Nat, HPow.hPow, Filter.atTop, nhds
Proof uses: Eq.mpr, Units, True, Filter.Eventually, Membership.mem, Set, Set.ofPred, HSub.hSub, id, Eq, congrArg, propext, Filter.HasBasis.tendsto_right_iff, IsValuativeTopology.hasBasis_nhds, Exists, ValuativeRel.exists_pow_valuation_lt, Filter.mp_mem, LE.le, Filter.eventually_ge_atTop, Filter.univ_mem' and 7 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem tendsto_pow_nhds_zero {x : k} (hx : valuation k x < 1) :
    Filter.Tendsto (fun n : ℕ ↦ x ^ n) Filter.atTop (nhds 0) := by
…
```
theorem TateCurve.summable_evalInt Documented declaration: summable_evalInt line 227 source
Source documentation
Every integral power series is evaluable on the open unit disc of a nonarchimedean local field: integers have valuation at most 1, so the terms have valuation at most |q|ⁿ → 0, and the nonarchimedean convergence criterion summable_of_valuation_le_pow applies with exponent function n ↦ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, ValuativeRel, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, PowerSeries, Int, Summable, Nat, HMul.hMul, LinearMap, RingHom.id, Unit, PowerSeries.coeff, HPow.hPow, SummationFilter.unconditional
Proof uses: TateCurve.summable_of_valuation_le_pow, Set.finite_Iio, Eq.mpr, LE.le, id, Eq, congrArg, map_mul, map_pow, Trans.trans, mul_le_mul_left, ValuativeRel.valuation_intCast_le_one, one_mul
97 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem summable_evalInt (q : k) (hq : valuation k q < 1) (F : ℤ⟦X⟧) :
    Summable fun n ↦ ((PowerSeries.coeff n F : ℤ) : k) * q ^ n :=
…
```
Mentions: TateCurve.X
theorem TateCurve.valuation_evalInt_le_pow Documented declaration: valuation_evalInt_le_pow line 240 source
Source documentation
If the first M coefficients of F vanish, its evaluation at a point of the open unit disc has valuation at most |q|^M: the partial sums satisfy the bound by the nonarchimedean triangle inequality, and it passes to the limit by the ultrametric isosceles principle (if v(σ - T) < v(T) and v(σ) < v(T) then v(T) ≤ max(v(σ), v(σ - T)) < v(T), absurd).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, ValuativeRel, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, PowerSeries, Int, Nat, Eq, LinearMap, RingHom.id, Unit, PowerSeries.coeff, LE.le, TateCurve.evalInt, HPow.hPow
Proof uses: Decidable.byContradiction, Not, Finset, Finset.sum, HMul.hMul, Valuation.map_sum_le, Membership.mem, Or, lt_or_ge, of_eq_true, Eq.trans, True, congrFun', congrArg, Int.cast_zero, MulZeroClass.zero_mul, map_zero, Eq.mpr, id, map_mul and 45 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_evalInt_le_pow (q : k) (hq : valuation k q < 1) {F : ℤ⟦X⟧}
    {M : ℕ} (hF : ∀ m < M, PowerSeries.coeff m F = 0) :
    valuation k (evalInt q F) ≤ valuation k q ^ M := by
…
```
Mentions: TateCurve.X, TateCurve.evalInt
theorem TateCurve.valuation_evalInt_eq Documented declaration: valuation_evalInt_eq line 279 source
Source documentation
The leading-term principle: if F = X + O(X²) then |F(q)| = |q| on the punctured open unit disc — ultrametrically the leading term dominates the tail, which has valuation at most |q|² by valuation_evalInt_le_pow.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, ValuativeRel, IsNonarchimedeanLocalField, Ne, OfNat.ofNat, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, PowerSeries, Int, Eq, RingHom, Unit, PowerSeries.constantCoeff, LinearMap, RingHom.id, PowerSeries.coeff, Nat and 1 more
Proof uses: HAdd.hAdd, HSub.hSub, PowerSeries.X, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring and 47 more
144 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_evalInt_eq (q : k) (hq0 : q ≠ 0) (hq : valuation k q < 1)
    {F : ℤ⟦X⟧} (h0 : PowerSeries.constantCoeff F = 0) (h1 : PowerSeries.coeff 1 F = 1) :
    valuation k (evalInt q F) = valuation k q := by
…
```
Mentions: TateCurve.X, TateCurve.evalInt
theorem TateCurve.evalInt_mul Evaluation of integral power series at a point of the open unit disc is multiplicative line 330 source
Source documentation
Evaluation of integral power series at a point of the open unit disc is multiplicative. Together with evalInt_add this makes evalInt q a ring homomorphism ℤ⟦X⟧ → k for each |q| < 1.
Proof: on the open unit disc, evalInt is the coercion to k of mathlib's topological power-series evaluation over the ring of integers (key below): q is an integer and topologically nilpotent (PowerSeries.HasEval), so PowerSeries.eval₂Hom converges in 𝒪[k] — which is linearly topologized, see the module comment above — and the continuous inclusion 𝒪[k] → k carries its defining sum (PowerSeries.hasSum_eval₂) to the sum defining evalInt. Multiplicativity is then map_mul of eval₂Hom.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, ValuativeRel, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, PowerSeries, Int, Eq, TateCurve.evalInt, HMul.hMul, Unit
Proof uses: UniformSpace, IsTopologicalAddGroup.rightUniformSpace, IsUniformAddGroup, isUniformAddGroup_of_addCommGroup, Subtype, Membership.mem, Subring, Valuation.integer, Topology.IsInducing, Topology.IsInducing.mk, rfl, Continuous, RingHom, Int.castRingHom, continuous_of_discreteTopology, PowerSeries.HasEval, Subtype.mk, LT.lt.le, Iff.mpr, Filter.Tendsto and 52 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem evalInt_mul (q : k) (hq : valuation k q < 1) (F G : ℤ⟦X⟧) :
    evalInt q (F * G) = evalInt q F * evalInt q G := by
…
```
Mentions: TateCurve.X, TateCurve.evalInt
theorem TateCurve.evalInt_pow Evaluation of integral power series at a point of the open unit disc respects powers: iterated evalInt_mul line 352 source
Source documentation
Evaluation of integral power series at a point of the open unit disc respects powers: iterated evalInt_mul.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, ValuativeRel, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, PowerSeries, Int, Nat, Eq, TateCurve.evalInt, HPow.hPow, Unit
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, tsum, HMul.hMul, LinearMap, RingHom.id, PowerSeries.coeff, SummationFilter.unconditional, ite, congrFun', SummationFilter, optParam, funext, pow_zero, PowerSeries.coeff_one, Int.cast_ite and 15 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem evalInt_pow (q : k) (hq : valuation k q < 1) (F : ℤ⟦X⟧) (m : ℕ) :
    evalInt q (F ^ m) = evalInt q F ^ m := by
…
```
Mentions: TateCurve.X, TateCurve.evalInt
def WeierstrassCurve.tateParameter Documented declaration: tateParameter line 378 source
Source documentation
The inverse of q ↦ j(q) (Silverman, ATAEC V.5.2): for |j| > 1, the unique q with 0 < |q| < 1 and j(q) = j, namely the evaluation q = j⁻¹ + 744j⁻² + 750420j⁻³ + ⋯ at j⁻¹ of the integral power series TateCurve.jInvReverse. Over a field complete with respect to a rank 1 nonarchimedean valuation the series converges for |j| > 1, since its coefficients are integers, hence of norm ≤ 1 (junk value for |j| ≤ 1).
Design note: unique existence cannot be turned into data in Lean without Classical.choose, so instead of stating V.5.2 as an ∃! we take the inverse map — an explicit power series, hence data on its own merits — as the definition. Uniqueness is then a round-trip identity (tateParameter (j(q)) = q, future work), and no choice is involved anywhere.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace
Proof uses: TateCurve.evalInt, Inv.inv, TateCurve.jInvReverse
7 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tateParameter (j : k) : k :=
…
```

FLT/KnownIn1980s/EllipticCurves/TateParameter.lean

The Tate parameter power series

Step 1: the formal series 1/j ∈ ℤ⟦q⟧ (TateCurve.jInv)

Step 2: formal compositional inversion (TateCurve.jInvReverse)

Step 3: evaluation (WeierstrassCurve.tateParameter)

`FLT/KnownIn1980s/EllipticCurves/TateParameter.lean`

Step 1: the formal series `1/j ∈ ℤ⟦q⟧` (`TateCurve.jInv`)

Step 2: formal compositional inversion (`TateCurve.jInvReverse`)

Step 3: evaluation (`WeierstrassCurve.tateParameter`)