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

14 declarations, 0 contain sorry, 0 declared as axioms

Module depth

The depth of a module: the supremum of the lengths of regular sequences, together with basic API.

Imports (10)

Imported by 2 files

def Module.depth Not sure if we should use IsRegular or IsWeaklyRegular line 41 source
Source documentation
Not sure if we should use IsRegular or IsWeaklyRegular. They agree for nontrivial finite modules over local rings. Using IsWeaklyRegular gives depth R 0 = ∞, which is the right one according to stacks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, ENat
Proof uses: SupSet.sSup, Set.ofPred, Exists, List, RingTheory.Sequence.IsWeaklyRegular, Membership.mem, Ideal, IsLocalRing.maximalIdeal, Eq, List.length
20 instances, coercions and auxiliary constants left out.
```
def Module.depth : ℕ∞ :=
…
```
instance (instance at line 46) line 46 source
lemma Module.length_le_depth line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, List, RingTheory.Sequence.IsWeaklyRegular, Membership.mem, Ideal, IsLocalRing.maximalIdeal, LE.le, ENat, List.length, Module.depth
Proof uses: le_sSup, Set.ofPred, Exists, Eq, Exists.intro, rfl
25 instances, coercions and auxiliary constants left out.
lemma Module.depth_of_subsingleton line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Subsingleton, Eq, ENat, Module.depth, Top.top
Proof uses: Eq.mpr, SupSet.sSup, Set.ofPred, Exists, List, RingTheory.Sequence.IsWeaklyRegular, Membership.mem, Ideal, IsLocalRing.maximalIdeal, List.length, id, congrArg, Module.depth.eq_1, LT.lt, And, Set, propext, sSup_eq_top, Nat, Iff.mp and 45 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Module.depth_of_isScalarTower line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Algebra, IsScalarTower, IsLocalHom, RingHom, Algebra.algebraMap, LE.le, ENat, Module.depth
Proof uses: sSup_le_sSup, Set.ofPred, Exists, List, RingTheory.Sequence.IsWeaklyRegular, Membership.mem, Ideal, IsLocalRing.maximalIdeal, Eq, List.length, Set, Exists.intro, List.map, Eq.mp, congrArg, Eq.symm, propext, RingTheory.Sequence.isWeaklyRegular_map_algebraMap_iff, Eq.mpr, Not and 14 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Module.depth_le_krullDim_support line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Nontrivial, Module.Finite, LE.le, WithBot, ENat, Module.depth, Order.krullDim, PrimeSpectrum, Module.support, Membership.mem, Set
Proof uses: Nonempty, Eq.mpr, Set.Nonempty, id, Eq, congrArg, propext, Set.nonempty_coe_sort, Ne, EmptyCollection.emptyCollection, Set.nonempty_iff_ne_empty, Not, ne_eq, Subsingleton, Module.support_eq_empty_iff, not_subsingleton_iff_nontrivial, WithBot.recBotCoe, Bot.bot, False, Eq.trans and 162 more
228 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
lemma Module.depth_le_dim_annihilator line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Nontrivial, Module.Finite, LE.le, WithBot, ENat, Module.depth, ringKrullDim, HasQuotient.Quotient, Ideal, Module.annihilator
Proof uses: Eq.mpr, Order.krullDim, PrimeSpectrum, PrimeSpectrum.zeroLocus, Membership.mem, Set, id, Eq, congrArg, ringKrullDim_quotient, Module.support, Eq.symm, Module.support_eq_zeroLocus, Module.depth_le_krullDim_support
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Module.depth_le_dim line 162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Nontrivial, Module.Finite, LE.le, WithBot, ENat, Module.depth, ringKrullDim
Proof uses: LE.le.trans, HasQuotient.Quotient, Ideal, Module.annihilator, Module.depth_le_dim_annihilator, ringKrullDim_quotient_le
15 instances, coercions and auxiliary constants left out.
lemma isSMulRegular_iff_of_free line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.Free, Nontrivial, Iff, IsSMulRegular
Proof uses: Module.Free.ChooseBasisIndex, Module.Basis, Module.Free.chooseBasis, Iff.intro, Eq, HSMul.hSMul, Nonempty.some, inferInstance, Nonempty, of_eq_true, Eq.trans, HMul.hMul, True, congr, congrArg, congrFun', id, eq_self, Eq.mp, Finsupp and 12 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma RingTheory.Sequence.isWeaklyRegular_of_subsingleton line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Subsingleton, List, RingTheory.Sequence.IsWeaklyRegular
Proof uses: Module.subsingleton, Iff.mpr, Fin, List.length, IsSMulRegular, HasQuotient.Quotient, Submodule, HSMul.hSMul, Ideal, Ideal.ofList, List.take, Top.top, GetElem.getElem, LT.lt, Nat, RingTheory.Sequence.isWeaklyRegular_iff_Fin, Eq, Subsingleton.elim
31 instances, coercions and auxiliary constants left out.
lemma RingTheory.Sequence.isWeaklyRegular_of_free_aux line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.Free, Nontrivial, List, Iff, RingTheory.Sequence.IsWeaklyRegular
Proof uses: Nat.recAux, Nat, Eq, List.length, OfNat.ofNat, of_eq_true, Eq.trans, True, congr, congrArg, List.nil, id, Eq.mp, iff_self, HAdd.hAdd, False.elim, False, And, and_false, Eq.symm and 39 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma RingTheory.Sequence.isWeaklyRegular_of_free line 214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.Free, Nontrivial, List, Iff, RingTheory.Sequence.IsWeaklyRegular
Proof uses: Module.Basis, Module.Free.ChooseBasisIndex, Module.Free.chooseBasis, Module.nontrivial, Eq.mpr, Finsupp, id, Eq, congrArg, propext, LinearEquiv.isWeaklyRegular_congr, Module.Basis.repr, RingTheory.Sequence.isWeaklyRegular_of_free_aux, Iff.rfl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Module.depth_le_of_free line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Module.Free, LE.le, ENat, Module.depth
Proof uses: Subsingleton, Nontrivial, Or, Eq, subsingleton_or_nontrivial, Or.inl, of_eq_true, Eq.trans, Top.top, True, congrArg, Module.depth_of_subsingleton, Or.inr, sSup_le_sSup, Set.ofPred, Exists, List, RingTheory.Sequence.IsWeaklyRegular, Membership.mem, Ideal and 8 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Module.faithfulSMul_of_depth_eq_ringKrullDim line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, IsDomain, Nontrivial, Module.Finite, LT.lt, WithBot, ENat, ringKrullDim, Top.top, Eq, Module.depth, FaithfulSMul
Proof uses: HasQuotient.Quotient, Ideal, Module.annihilator, Iff.mpr, Ne, Ideal.Quotient.nontrivial_iff, Eq.mpr, Not, id, congrArg, ne_eq, Submodule.annihilator, Submodule, Eq.symm, Submodule.annihilator_top, Bot.bot, propext, Submodule.annihilator_eq_top_iff, top_ne_bot, Module.annihilator_eq_bot and 65 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.