S02_Algebraic_Structures.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 9 curated AI-written annotations and 7 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 Mathematics in Lean documentation, Pinned Mathematics in Lean textbook

30 declarations, 3 contain sorry, 0 declared as axioms

Imports (2)

Imported by 1 file

MIL.lean

structure C06S02.Group₁ line 6 source
no axioms what this means
structure C06S02.Grp₁ line 15 source
no axioms what this means
example C06S02.(example at line 32) line 32 source
example C06S02.(example at line 35) line 35 source
example C06S02.(example at line 38) line 38 source
example C06S02.(example at line 43) line 43 source
def C06S02.permGroup line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: C06S02.Group₁, Equiv.Perm
Proof uses: C06S02.Group₁.mk, Equiv.trans, Equiv.refl, Equiv.symm, Equiv.refl_trans, Equiv.trans_refl, Equiv.self_trans_symm
1 instances, coercions and auxiliary constants left out.
structure C06S02.AddGroup₁ line 56 source
no axioms what this means

Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean:6 (same statement text; different proof or body). Qualify references as C06S02.AddGroup₁@path.
structure C06S02.Point fill in the rest line 60 source
Source comment
fill in the rest

standard axioms: Classical.choice, Quot.sound, propext what this means

Also declared: MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean:16 (same declaration text).
```
structure Point where
…
```
def C06S02.Point.add line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: C06S02.Point
Proof uses: C06S02.Point.mk, HAdd.hAdd, Real, C06S02.Point.x, C06S02.Point.y, C06S02.Point.z
2 instances, coercions and auxiliary constants left out.

Also declared: MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean:23 (same declaration text).
def C06S02.Point.neg sorry line 70 source
depends on sorry what this means
Statement uses: C06S02.Point
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean:26 (same statement text; different proof or body). Qualify references as C06S02.Point.neg@path.
def C06S02.Point.zero sorry line 72 source
depends on sorry what this means
Statement uses: C06S02.Point
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean:29 (same statement text; different proof or body). Qualify references as C06S02.Point.zero@path.
def C06S02.Point.addGroupPoint sorry line 74 source
depends on sorry what this means
Statement uses: C06S02.AddGroup₁, C06S02.Point
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean:32 (same statement text; different proof or body). Qualify references as C06S02.Point.addGroupPoint@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
example C06S02.(example at line 87) line 87 source
example C06S02.(example at line 89) line 89 source
example C06S02.(example at line 92) line 92 source
class C06S02.Group₂ line 97 source
no axioms what this means
instance C06S02.(instance at line 106) line 106 source
def C06S02.mySquare line 117 source
no axioms what this means
Statement uses: C06S02.Group₂
Proof uses: C06S02.Group₂.mul
example C06S02.(example at line 125) line 125 source
example C06S02.(example at line 128) line 128 source
instance C06S02.(instance at line 133) line 133 source
example C06S02.(example at line 137) line 137 source
instance C06S02.(instance at line 140) line 140 source
example C06S02.(example at line 147) line 147 source
instance C06S02.(instance at line 152) line 152 source
instance C06S02.(instance at line 155) line 155 source
instance C06S02.(instance at line 158) line 158 source
def C06S02.foo line 166 source
standard axioms: Quot.sound what this means
Statement uses: Equiv.Perm, Eq, HMul.hMul, OfNat.ofNat, Inv.inv, Equiv.trans, Equiv.symm, Equiv.refl
Proof uses: rfl
10 instances, coercions and auxiliary constants left out.
class C06S02.AddGroup₂ line 171 source
no axioms what this means

Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean:43 (same statement text; different proof or body). Qualify references as C06S02.AddGroup₂@path.