Aut.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

8 declarations, 0 contain sorry, 0 declared as axioms

Automorphisms of an elliptic curve with `j ∉ {0, 1728}`

Proposed new Mathlib file Mathlib.AlgebraicGeometry.EllipticCurve.Aut.

Let E be an elliptic curve over a field K. Over a field, isomorphisms of Weierstrass curves are exactly the admissible changes of variables WeierstrassCurve.VariableChange K, acting via •; the automorphisms of E are therefore the C : VariableChange K with C • E = E. This file proves the classical fact (Silverman, The Arithmetic of Elliptic Curves, III.10) that if j(E) ∉ {0, 1728} then the only automorphisms of E are ±1, uniformly in the characteristic.

Main definitions and statements

WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq : if j(E) ∉ {0, 1728} then any C : VariableChange K with C • E = E equals 1 or negVariableChange E.
WeierstrassCurve.autGroup E : the automorphism group of E, as the stabiliser of E under the action of VariableChange K.
WeierstrassCurve.autGroupMulEquiv : for j(E) ∉ {0, 1728}, the (computable) isomorphism autGroup E ≃* Multiplicative (ZMod 2).

Implementation notes

The proof is broken into pieces. j ∉ {0, 1728} is equivalent to c₄ ≠ 0 and c₆ ≠ 0 (j_eq_zero_iff and c₆_eq_zero_iff_j_eq_1728). From the transformation laws of c₄ and c₆ one gets u² = 1 (u_eq_one_or_eq_neg_one), which reduces everything to the case u = 1. There r = 0 follows from the transformation laws of b₄, b₆, b₈ (r_eq_zero_of_u_eq_one), and then s, t are read off from those of a₁, a₂, a₃, a₄ (eq_one_or_eq_negVariableChange_of_u_eq_one, where the negVariableChange value can occur only in characteristic 2).

Imports (2)

Imported by 2 files

lemma WeierstrassCurve.r_eq_zero_of_u_eq_one An automorphism C of E with C.u = 1 has no x-translation: C.r = 0 line 59 source
Source documentation
An automorphism C of E with C.u = 1 has no x-translation: C.r = 0. This follows from the transformation laws of b₄, b₆, b₈ together with c₆ ≠ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Ne, WeierstrassCurve.c₆, OfNat.ofNat, WeierstrassCurve.VariableChange, Eq, Units, WeierstrassCurve.VariableChange.u, HSMul.hSMul, WeierstrassCurve.VariableChange.r
Proof uses: WeierstrassCurve.b₄, congrArg, WeierstrassCurve.b₆, WeierstrassCurve.b₈, Eq.mp, HSub.hSub, HAdd.hAdd, Neg.neg, HPow.hPow, Nat, WeierstrassCurve.b₂, HMul.hMul, WeierstrassCurve.c₆.eq_1, congrFun', Eq.trans, Inv.inv, WeierstrassCurve.variableChange_b₄, inv_one, one_pow, one_mul and 2 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma r_eq_zero_of_u_eq_one (hc6 : E.c₆ ≠ 0) {C : VariableChange K} (hu : C.u = 1)
    (hCE : C • E = E) :
    C.r = 0 := by
…
```
lemma WeierstrassCurve.eq_one_or_eq_negVariableChange_of_u_eq_one An automorphism C of E with C.u = 1 is either the identity or negVariableChange E line 73 source
Source documentation
An automorphism C of E with C.u = 1 is either the identity or negVariableChange E. After r_eq_zero_of_u_eq_one, the a₁ and a₃ laws give 2s = 2t = 0; in characteristic ≠ 2 this forces s = t = 0, and in characteristic 2 the a₂, a₄ laws pin (s, t) down to either (0, 0) or (-a₁, -a₃).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Ne, WeierstrassCurve.c₄, OfNat.ofNat, WeierstrassCurve.c₆, WeierstrassCurve.VariableChange, Eq, Units, WeierstrassCurve.VariableChange.u, HSMul.hSMul, Or, WeierstrassCurve.negVariableChange
Proof uses: WeierstrassCurve.VariableChange.r, WeierstrassCurve.r_eq_zero_of_u_eq_one, WeierstrassCurve.a₁, And, WeierstrassCurve.a₂, WeierstrassCurve.a₃, WeierstrassCurve.a₄, WeierstrassCurve.a₆, Iff.mp, WeierstrassCurve.ext_iff, Nat, eq_or_ne, Eq.mp, HSub.hSub, HPow.hPow, HAdd.hAdd, HMul.hMul, WeierstrassCurve.b₄, congrArg, WeierstrassCurve.b₄.eq_1 and 84 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma eq_one_or_eq_negVariableChange_of_u_eq_one (hc4 : E.c₄ ≠ 0) (hc6 : E.c₆ ≠ 0)
    {C : VariableChange K} (hu : C.u = 1) (hCE : C • E = E) :
    C = 1 ∨ C = E.negVariableChange := by
…
```
lemma WeierstrassCurve.u_eq_one_or_eq_neg_one The u-coefficient of an automorphism C of E (with c₄, c₆ ≠ 0) satisfies u² = 1: the c₄ and c₆ laws give u⁴ = u⁶ = 1 line 100 source
Source documentation
The u-coefficient of an automorphism C of E (with c₄, c₆ ≠ 0) satisfies u² = 1: the c₄ and c₆ laws give u⁴ = u⁶ = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Ne, WeierstrassCurve.c₄, OfNat.ofNat, WeierstrassCurve.c₆, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, Or, Units, WeierstrassCurve.VariableChange.u, Neg.neg
Proof uses: HPow.hPow, Nat, congrArg, Eq.mp, Inv.inv, propext, inv_eq_one, inv_pow, HMul.hMul, mul_eq_right₀, Units.val_inv_eq_inv_val, WeierstrassCurve.variableChange_c₄, WeierstrassCurve.variableChange_c₆, Mathlib.Tactic.LinearCombination.eq_of_eq, HAdd.hAdd, Mathlib.Tactic.LinearCombination.add_eq_eq, Eq.symm, Mathlib.Tactic.LinearCombination.mul_const_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq and 60 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma u_eq_one_or_eq_neg_one (hc4 : E.c₄ ≠ 0) (hc6 : E.c₆ ≠ 0) {C : VariableChange K}
    (hCE : C • E = E) : C.u = 1 ∨ C.u = -1 := by
…
```
theorem WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq_of_c₄_ne_zero If c₄ ≠ 0 and c₆ ≠ 0 then the only admissible changes of variables fixing E are 1 and negVariableChange E line 116 source
Source documentation
If c₄ ≠ 0 and c₆ ≠ 0 then the only admissible changes of variables fixing E are 1 and negVariableChange E. This is the form of Aut(E) = {±1} phrased via c₄, c₆ (equivalent to j ∉ {0, 1728} for an elliptic curve, see eq_one_or_eq_negVariableChange_of_smul_eq).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Ne, WeierstrassCurve.c₄, OfNat.ofNat, WeierstrassCurve.c₆, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, Or, WeierstrassCurve.negVariableChange
Proof uses: Units, WeierstrassCurve.VariableChange.u, Neg.neg, WeierstrassCurve.u_eq_one_or_eq_neg_one, WeierstrassCurve.eq_one_or_eq_negVariableChange_of_u_eq_one, HMul.hMul, Eq.mpr, id, congrArg, rfl, WeierstrassCurve.negVariableChange_u, neg_one_mul, neg_neg, Eq.refl, SemigroupAction.mul_smul, WeierstrassCurve.negVariableChange_smul_self, Eq.symm, mul_assoc, WeierstrassCurve.negVariableChange_mul_self, one_mul and 3 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem eq_one_or_eq_negVariableChange_of_smul_eq_of_c₄_ne_zero (hc4 : E.c₄ ≠ 0) (hc6 : E.c₆ ≠ 0)
    {C : VariableChange K} (hC : C • E = E) : C = 1 ∨ C = E.negVariableChange := by
…
```
theorem WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq If j(E) ∉ {0, 1728} then the only admissible changes of variables fixing E are 1 and negVariableChange E; that is, Aut(E) = {±1} line 134 source
Source documentation
If j(E) ∉ {0, 1728} then the only admissible changes of variables fixing E are 1 and negVariableChange E; that is, Aut(E) = {±1}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, Ne, WeierstrassCurve.j, OfNat.ofNat, Nat, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, Or, WeierstrassCurve.negVariableChange
Proof uses: WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq_of_c₄_ne_zero, Iff.mp, Not, WeierstrassCurve.c₄, Iff.not, WeierstrassCurve.j_eq_zero_iff, Iff.mpr, WeierstrassCurve.c₆, WeierstrassCurve.c₆_eq_zero_iff_j_eq_1728
43 instances, coercions and auxiliary constants left out.
```
theorem eq_one_or_eq_negVariableChange_of_smul_eq [E.IsElliptic] (hj₀ : E.j ≠ 0)
    (hj₁₇₂₈ : E.j ≠ 1728) {C : VariableChange K} (hC : C • E = E) :
    C = 1 ∨ C = E.negVariableChange :=
…
```
def WeierstrassCurve.autGroup The automorphism group of a Weierstrass curve E over a field: the admissible changes of variables fixing E, i.e. the stabiliser of E under the action of VariableChange K line 145 source
Source documentation
The automorphism group of a Weierstrass curve E over a field: the admissible changes of variables fixing E, i.e. the stabiliser of E under the action of VariableChange K.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Subgroup, WeierstrassCurve.VariableChange
Proof uses: MulAction.stabilizer
5 instances, coercions and auxiliary constants left out.
```
def autGroup : Subgroup (VariableChange K) := stabilizer (VariableChange K) E
```
lemma WeierstrassCurve.mem_autGroup line 147 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.VariableChange, Iff, Membership.mem, Subgroup, WeierstrassCurve.autGroup, Eq, HSMul.hSMul
Proof uses: Iff.rfl
10 instances, coercions and auxiliary constants left out.
def WeierstrassCurve.autGroupMulEquiv Aut(E) ≅ ℤ/2 for j(E) ∉ {0, 1728} line 154 source
Source documentation
Aut(E) ≅ ℤ/2 for j(E) ∉ {0, 1728}. The automorphism group of E is {±1}, so it is isomorphic to Multiplicative (ZMod 2): it has exactly two elements — 1 and negVariableChange E (eq_one_or_eq_negVariableChange_of_smul_eq), distinct by negVariableChange_ne_one. The isomorphism sends negVariableChange E to Multiplicative.ofAdd 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, DecidableEq, WeierstrassCurve.IsElliptic, Ne, WeierstrassCurve.j, OfNat.ofNat, Nat, MulEquiv, Subtype, WeierstrassCurve.VariableChange, Membership.mem, Subgroup, WeierstrassCurve.autGroup, Multiplicative, ZMod
Proof uses: mulEquivMultiplicativeZModTwo, Subtype.mk, WeierstrassCurve.negVariableChange, WeierstrassCurve.negVariableChange_smul_self
47 instances, coercions and auxiliary constants left out.
```
def autGroupMulEquiv [DecidableEq K] [E.IsElliptic] (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728) :
    E.autGroup ≃* Multiplicative (ZMod 2) :=
…
```

FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Aut.lean

Automorphisms of an elliptic curve with j ∉ {0, 1728}

Main definitions and statements

Implementation notes

`FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Aut.lean`

Automorphisms of an elliptic curve with `j ∉ {0, 1728}`