Coset.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 10 curated AI-written annotations and 7190 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, Formal Conjectures paper, arXiv v1

8 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

Imported by 1 file

FormalConjecturesForMathlib.lean

def maxCosetDim line 21 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, Set, Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, AffineSubspace, LE.le, Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction
18 instances, coercions and auxiliary constants left out.
theorem maxCosetDim_univ The maximum coset dimension in the entire vector space $V$ is exactly the dimension of $V$ line 30 source
Source documentation
The maximum coset dimension in the entire vector space $V$ is exactly the dimension of $V$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, Eq, Nat, maxCosetDim, Set.univ, Module.finrank
Proof uses: id, le_antisymm, SupSet.sSup, Set.ofPred, Exists, AffineSubspace, LE.le, Set, Subtype, Membership.mem, Submodule, AffineSubspace.direction, csSup_le, Exists.intro, OfNat.ofNat, Bot.bot, of_eq_true, Eq.trans, True, propext and 16 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem maxCosetDim_univ (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] : maxCosetDim K V (Set.univ : Set V) = Module.finrank K V := by
…
```
Mentions: maxCosetDim
theorem maxCosetDim_empty The maximum coset dimension in the empty set $\emptyset$ is $0$ line 49 source
Source documentation
The maximum coset dimension in the empty set $\emptyset$ is $0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, Eq, Nat, maxCosetDim, EmptyCollection.emptyCollection, Set, OfNat.ofNat
Proof uses: id, Set.ofPred, Exists, AffineSubspace, LE.le, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, Singleton.singleton, Set.ext, Eq.mpr, Iff, congr, congrArg, congrFun', funext, propext, exists_prop_congr and 16 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem maxCosetDim_empty (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] : maxCosetDim K V (∅ : Set V) = 0 := by
…
```
Mentions: maxCosetDim
theorem maxCosetDim_mono If $A \subseteq B$, then the maximum coset dimension achievable in $A$ cannot exceed the maximum coset dimension achievable in $B$ line 68 source
Source documentation
If $A \subseteq B$, then the maximum coset dimension achievable in $A$ cannot exceed the maximum coset dimension achievable in $B$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, Set, LE.le, Nat, maxCosetDim
Proof uses: id, csSup_le, Set.ofPred, Exists, AffineSubspace, Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, SupSet.sSup, Exists.intro, OfNat.ofNat, Bot.bot, of_eq_true, Eq.trans, True, propext, exists_prop_congr and 11 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem maxCosetDim_mono (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] {A B : Set V} (h : A ⊆ B) :
    maxCosetDim K V A ≤ maxCosetDim K V B := by
…
```
Mentions: maxCosetDim
theorem maxCosetDim_affineSubspace If the target set $A$ is already an affine subspace, the function returns exactly the rank of its direction line 91 source
Source documentation
If the target set $A$ is already an affine subspace, the function returns exactly the rank of its direction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, AffineSubspace, Eq, Nat, maxCosetDim, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction
Proof uses: id, le_antisymm, SupSet.sSup, Set.ofPred, Exists, LE.le, Set, csSup_le, Exists.intro, OfNat.ofNat, Bot.bot, of_eq_true, Eq.trans, True, propext, exists_prop_congr, Iff.of_eq, congrFun', congrArg, AffineSubspace.direction_bot and 13 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem maxCosetDim_affineSubspace (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (S : AffineSubspace K V) :
    maxCosetDim K V (S : Set V) = Module.finrank K S.direction := by
…
```
Mentions: maxCosetDim
theorem maxCosetDim_singleton Similar to the empty set, a set containing exactly one vector should yield a maximum dimension of 0 line 112 source
Source documentation
Similar to the empty set, a set containing exactly one vector should yield a maximum dimension of 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, Eq, Nat, maxCosetDim, Singleton.singleton, Set, OfNat.ofNat
Proof uses: id, Set.ofPred, Exists, AffineSubspace, LE.le, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, Set.ext, Eq.mpr, Iff, congrArg, Iff.intro, Bot.bot, LT.lt, Or, eq_bot_or_bot_lt, AffineSubspace.direction_bot and 31 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
theorem maxCosetDim_singleton (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (v : V) : maxCosetDim K V ({v} : Set V) = 0 := by
…
```
Mentions: maxCosetDim
lemma maxCosetDim_vadd_le line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, Set, LE.le, Nat, maxCosetDim, HVAdd.hVAdd
Proof uses: id, csSup_le, Set.ofPred, Exists, AffineSubspace, Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, SupSet.sSup, Exists.intro, OfNat.ofNat, Bot.bot, of_eq_true, Eq.trans, True, propext, exists_prop_congr and 26 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
theorem maxCosetDim_vadd Translating a set by a vector does not change its maximum coset dimension line 173 source
Source documentation
Translating a set by a vector does not change its maximum coset dimension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, AddCommGroup, Module, FiniteDimensional, Set, Eq, Nat, maxCosetDim, HVAdd.hVAdd
Proof uses: le_antisymm, maxCosetDim_vadd_le, LE.le, Neg.neg, Set.ext, Iff.intro, Membership.mem, And, id, Eq.mpr, HAdd.hAdd, congrArg, neg_add_cancel_left, Exists.intro, And.intro, rfl, Eq.refl, Eq.mp
37 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
theorem maxCosetDim_vadd (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] (v : V) (A : Set V) :
    maxCosetDim K V (v +ᵥ A) = maxCosetDim K V A := by
…
```
Mentions: maxCosetDim