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

42 declarations, 0 contain sorry, 0 declared as axioms

Finiteness of algebraic structures on finite types

Instances asserting that the type of monoid / group / ring / … structures on a fixed finite type is itself finite.

Imports (6)

Imported by 2 files

instance (instance at line 26) line 26 source
instance (instance at line 31) line 31 source
instance (instance at line 36) line 36 source
instance (instance at line 39) line 39 source
instance (instance at line 47) line 47 source
def ModuleTypeCardLT The type of all finite R-modules of cardinality less than N, presented as a sigma type over Fin N line 66 source
Source documentation
The type of all finite R-modules of cardinality less than N, presented as a sigma type over Fin N.

no axioms what this means
Statement uses: Ring, Nat
Proof uses: Sigma, Fin, AddCommGroup, Module
3 instances, coercions and auxiliary constants left out.
```
def ModuleTypeCardLT (N : ℕ) : Type _ :=
…
```
instance (instance at line 69) line 69 source
instance (instance at line 72) line 72 source
instance (instance at line 74) line 74 source
def ModuleTypeCardLT.ofModule line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Nat, AddCommGroup, Module, Finite, LT.lt, Nat.card, ModuleTypeCardLT
Proof uses: Sigma.mk, Fin, Sigma, Fin.mk, Equiv.addCommGroup, Equiv.symm, Finite.equivFin, Equiv.module'
7 instances, coercions and auxiliary constants left out.
def ModuleTypeCardLT.equivOfModule line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Nat, AddCommGroup, Module, Finite, LT.lt, Nat.card, LinearEquiv, RingHom.id, Fin, Sigma.fst, Sigma, ModuleTypeCardLT.ofModule
Proof uses: LinearEquiv.symm, Equiv.addCommMonoid, Equiv.symm, Equiv, Finite.equivFin, Equiv.module', Equiv.linearEquiv'
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance (instance at line 97) line 97 source
def AlgebraTypeCardLT The type of all finite R-algebras of cardinality less than N, presented as a sigma type over Fin N line 105 source
Source documentation
The type of all finite R-algebras of cardinality less than N, presented as a sigma type over Fin N.

no axioms what this means
Statement uses: CommRing, Nat
Proof uses: Sigma, Fin, Ring, Algebra
3 instances, coercions and auxiliary constants left out.
```
def AlgebraTypeCardLT (N : ℕ) : Type _ :=
…
```
instance (instance at line 108) line 108 source
instance (instance at line 111) line 111 source
instance (instance at line 113) line 113 source
def AlgebraTypeCardLT.ofAlgebra line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Nat, Ring, Algebra, Finite, LT.lt, Nat.card, AlgebraTypeCardLT
Proof uses: Sigma.mk, Fin, Sigma, Fin.mk, Equiv.ring, Equiv.symm, Finite.equivFin, Equiv.algebra
7 instances, coercions and auxiliary constants left out.
def AlgebraTypeCardLT.equivOfAlgebra line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Nat, Ring, Algebra, Finite, LT.lt, Nat.card, AlgEquiv, Fin, Sigma.fst, Sigma, AlgebraTypeCardLT.ofAlgebra
Proof uses: AlgEquiv.symm, Equiv.semiring, Equiv.symm, Equiv, Finite.equivFin, Equiv.algebra, Equiv.algEquiv
10 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance (instance at line 135) line 135 source
instance (instance at line 145) line 145 source
def TopologicalModuleTypeCardLT The type of all finite Hausdorff topological R-modules of cardinality less than N, with continuous scalar multiplication line 158 source
Source documentation
The type of all finite Hausdorff topological R-modules of cardinality less than N, with continuous scalar multiplication.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Nat
Proof uses: PSigma, Fin, AddCommGroup, T2Space, Module, ContinuousSMul
15 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def TopologicalModuleTypeCardLT (N : ℕ) : Type _ :=
…
```
instance (instance at line 162) line 162 source
instance (instance at line 170) line 170 source
instance (instance at line 174) line 174 source
instance (instance at line 175) line 175 source
instance (instance at line 176) line 176 source
instance (instance at line 177) line 177 source
instance (instance at line 178) line 178 source
def TopologicalModuleTypeCardLT.ofModule line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Nat, AddCommGroup, Module, T2Space, ContinuousSMul, Finite, LT.lt, Nat.card, TopologicalModuleTypeCardLT
Proof uses: PSigma.mk, Fin, PSigma, Fin.mk, Equiv.addCommGroup, Equiv.symm, Finite.equivFin, TopologicalSpace.coinduced, Equiv, inferInstance, Equiv.module'
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def TopologicalModuleTypeCardLT.equivOfModule line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Nat, AddCommGroup, Module, T2Space, ContinuousSMul, Finite, LT.lt, Nat.card, ContinuousLinearEquiv, RingHom.id, Fin, PSigma.fst, PSigma, TopologicalModuleTypeCardLT.ofModule
Proof uses: LinearEquiv, Sigma.fst, Sigma, ModuleTypeCardLT.ofModule, Equiv.addCommMonoid, Equiv.symm, Equiv, Finite.equivFin, Equiv.module', LinearEquiv.symm, Equiv.linearEquiv', Homeomorph, inferInstance, Equiv.toHomeomorph, ContinuousLinearEquiv.mk
47 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance (instance at line 222) line 222 source
def TopologicalAlgebraTypeCardLT The type of all finite Hausdorff topological R-algebras of cardinality less than N, with continuous scalar multiplication line 236 source
Source documentation
The type of all finite Hausdorff topological R-algebras of cardinality less than N, with continuous scalar multiplication.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Nat
Proof uses: PSigma, Fin, Ring, T2Space, Algebra, ContinuousSMul
4 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def TopologicalAlgebraTypeCardLT (N : ℕ) :
    Type _ :=
…
```
instance (instance at line 241) line 241 source
instance (instance at line 249) line 249 source
instance (instance at line 253) line 253 source
instance (instance at line 254) line 254 source
instance (instance at line 255) line 255 source
instance (instance at line 256) line 256 source
instance (instance at line 257) line 257 source
def TopologicalAlgebraTypeCardLT.ofAlgebra line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Nat, Ring, Algebra, T2Space, ContinuousSMul, Finite, LT.lt, Nat.card, TopologicalAlgebraTypeCardLT
Proof uses: PSigma.mk, Fin, PSigma, Fin.mk, Equiv.ring, Equiv.symm, Finite.equivFin, TopologicalSpace.coinduced, Equiv, inferInstance, Equiv.algebra
14 instances, coercions and auxiliary constants left out.
def TopologicalAlgebraTypeCardLT.equivOfAlgebra line 278 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Nat, Ring, Algebra, T2Space, ContinuousSMul, Finite, LT.lt, Nat.card, AlgEquiv, Fin, PSigma.fst, PSigma, TopologicalAlgebraTypeCardLT.ofAlgebra
Proof uses: AlgEquiv.symm, Sigma.fst, Sigma, AlgebraTypeCardLT.ofAlgebra, Equiv.semiring, Equiv.symm, Equiv, Finite.equivFin, Equiv.algebra, Equiv.algEquiv
12 instances, coercions and auxiliary constants left out.
lemma TopologicalAlgebraTypeCardLT.isHomeomorph_equivOfAlgebra line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Nat, Ring, Algebra, T2Space, ContinuousSMul, Finite, LT.lt, Nat.card, IsHomeomorph, Fin, PSigma.fst, PSigma, TopologicalAlgebraTypeCardLT.ofAlgebra, AlgEquiv, TopologicalAlgebraTypeCardLT.equivOfAlgebra
Proof uses: Homeomorph.isHomeomorph, inferInstance, Equiv.toHomeomorph, Finite.equivFin, Set, Iff.rfl, IsOpen, Set.preimage, Equiv
19 instances, coercions and auxiliary constants left out.