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

10 declarations, 5 contain sorry, 0 declared as axioms

Kaplansky's Conjectures

Reference: Wikipedia

Throughout, "torsion-free" means that the identity is the only element of finite order (Monoid.IsTorsionFree). This is weaker than Mathlib's IsMulTorsionFree, which asks for uniqueness of roots and fails for the Promislow group below.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

theorem Kaplansky.zero_divisor_conjecture The zero-divisor conjecture If G is torsion-free, then the group algebra K[G] has no non-trivial zero divisors sorry line 44 source
Source documentation
The zero-divisor conjecture
If G is torsion-free, then the group algebra K[G] has no non-trivial zero divisors.

depends on sorry what this means
Statement uses: Field, Group, Monoid.IsTorsionFree, NoZeroDivisors, MonoidAlgebra
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem zero_divisor_conjecture : NoZeroDivisors (MonoidAlgebra K G) := by
…
```
theorem Kaplansky.idempotent_conjecture The idempotent conjecture If G is torsion-free, then K[G] has no non-trivial idempotents sorry line 53 source
Source documentation
The idempotent conjecture
If G is torsion-free, then K[G] has no non-trivial idempotents.

depends on sorry what this means
Statement uses: Field, Group, Monoid.IsTorsionFree, MonoidAlgebra, IsIdempotentElem, Or, Eq, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem idempotent_conjecture (a : MonoidAlgebra K G) (h : IsIdempotentElem a) :
    a = 0 ∨ a = 1 := by
…
```
def Kaplansky.IsTrivialUnit A unit in K[G] is trivial if it is exactly of the form kg where: - k is a unit in the base field K - g is an element of the group G line 63 source
Source documentation
A unit in K[G] is trivial if it is exactly of the form kg where:
- k is a unit in the base field K
- g is an element of the group G
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, MonoidAlgebra
Proof uses: Exists, Units, Eq, MonoidAlgebra.single
8 instances, coercions and auxiliary constants left out.
```
def IsTrivialUnit (u : MonoidAlgebra K G) : Prop :=
…
```
lemma Kaplansky.IsTrivialUnit.isUnit line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Group, MonoidAlgebra, Kaplansky.IsTrivialUnit, IsUnit
Proof uses: Units, Exists, Eq, MonoidAlgebra.single, IsUnit.map, MonoidHom, Prod, MonoidAlgebra.singleHom, Prod.mk, Iff.mpr, And, Prod.fst, Prod.snd, Prod.isUnit_iff, And.intro, Units.isUnit, Group.isUnit, Eq.symm
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
abbrev Kaplansky.PromislowGroup The Promislow group ⟨ a, b | b⁻¹a²ba², a⁻¹b²ab² ⟩ line 78 source
Source documentation
The Promislow group ⟨ a, b | b⁻¹a²ba², a⁻¹b²ab² ⟩

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: PresentedGroup, Fin, OfNat.ofNat, Nat, Insert.insert, FreeGroup, Set, HMul.hMul, Inv.inv, FreeGroup.of, Singleton.singleton
8 instances, coercions and auxiliary constants left out.
```
abbrev PromislowGroup : Type :=
…
```
lemma Kaplansky.promislow_group_is_torsionfree The Promislow group is torsion-free sorry line 87 source
Source documentation
The Promislow group is torsion-free.

depends on sorry what this means
Statement uses: Monoid.IsTorsionFree, Kaplansky.PromislowGroup, Fin, OfNat.ofNat, Nat, Insert.insert, FreeGroup, Set, HMul.hMul, Inv.inv, FreeGroup.of, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma promislow_group_is_torsionfree :
    Monoid.IsTorsionFree PromislowGroup := by
…
```
Mentions: Monoid.IsTorsionFree, Kaplansky.PromislowGroup
theorem Kaplansky.UnitConjecture.counterexamples.i If $P$ is the Promislow group, then the group ring $\mathbb{F}_p[P]$ has a non-trivial unit sorry line 95 source
Source documentation
If $P$ is the Promislow group, then the group ring $\mathbb{F}_p[P]$ has a non-trivial unit.

depends on sorry what this means
Statement uses: Nat, Fact, Nat.Prime, Exists, Units, MonoidAlgebra, ZMod, Kaplansky.PromislowGroup, Fin, OfNat.ofNat, Insert.insert, FreeGroup, Set, HMul.hMul, Inv.inv, FreeGroup.of, Singleton.singleton, Not, Kaplansky.IsTrivialUnit
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem UnitConjecture.counterexamples.i (p : ℕ) [hp : Fact p.Prime] :
    ∃ (u : (MonoidAlgebra (ZMod p) PromislowGroup)ˣ), ¬IsTrivialUnit u.val := by
…
```
Mentions: Kaplansky.PromislowGroup, Kaplansky.IsTrivialUnit
theorem Kaplansky.UnitConjecture.counterexamples.ii If $P$ is the Promislow group, then the group ring $\mathbb{C}[P]$ has a non-trivial unit sorry line 103 source
Source documentation
If $P$ is the Promislow group, then the group ring $\mathbb{C}[P]$ has a non-trivial unit.

depends on sorry what this means
Statement uses: Exists, Units, MonoidAlgebra, Complex, Kaplansky.PromislowGroup, Fin, OfNat.ofNat, Nat, Insert.insert, FreeGroup, Set, HMul.hMul, Inv.inv, FreeGroup.of, Singleton.singleton, Not, Kaplansky.IsTrivialUnit
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem UnitConjecture.counterexamples.ii :
    ∃ (u : (MonoidAlgebra ℂ PromislowGroup)ˣ), ¬IsTrivialUnit u.val := by
…
```
Mentions: Kaplansky.PromislowGroup, Kaplansky.IsTrivialUnit
theorem Kaplansky.counter_unit_conjecture The Unit Conjecture is false line 116 source
Source documentation
The Unit Conjecture is false.
At least there is a counterexample for any prime and zero characteristic: [Mu21] Murray, A. (2021). More Counterexamples to the Unit Conjecture for Group Rings. [Pa21] Passman, D. (2021). On the counterexamples to the unit conjecture for group rings. [Ga24] Gardam, G. (2024). Non-trivial units of complex group rings.

depends on sorry what this means
Statement uses: Exists, Group, Monoid.IsTorsionFree, Nat, Or, Eq, OfNat.ofNat, Nat.Prime, Field, CharP, Units, MonoidAlgebra, Not, Kaplansky.IsTrivialUnit
Proof uses: Exists.intro, Kaplansky.PromislowGroup, Fin, Insert.insert, FreeGroup, Set, HMul.hMul, Inv.inv, FreeGroup.of, Singleton.singleton, Kaplansky.promislow_group_is_torsionfree, Or.by_cases, Complex, inferInstance, Kaplansky.UnitConjecture.counterexamples.ii, Eq.symm, Fact, Fact.mk, ZMod, Kaplansky.UnitConjecture.counterexamples.i
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem counter_unit_conjecture :
    ∃ (G : Type) (_ : Group G) (_ : Monoid.IsTorsionFree G),
    ∀ (p : ℕ) (_ : p = 0 ∨ p.Prime),
    ∃ (K : Type) (_ : Field K) (_ :  CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit u.val :=
…
```
Mentions: Monoid.IsTorsionFree, Kaplansky.IsTrivialUnit
theorem Kaplansky.counter_unit_conjecture_weak There is a counterexample to Unit Conjecture in any characteristic line 128 source
Source documentation
There is a counterexample to Unit Conjecture in any characteristic.

depends on sorry what this means
Statement uses: Nat, Or, Eq, OfNat.ofNat, Nat.Prime, Exists, Group, Monoid.IsTorsionFree, Field, CharP, Units, MonoidAlgebra, Not, Kaplansky.IsTrivialUnit
Proof uses: Kaplansky.counter_unit_conjecture, Exists.intro
27 instances, coercions and auxiliary constants left out.
```
theorem counter_unit_conjecture_weak (p : ℕ) (hp : p = 0 ∨ p.Prime) :
    ∃ (G : Type) (_ : Group G) (_ : Monoid.IsTorsionFree G)
      (K : Type) (_ : Field K) (_ :  CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit u.val :=
…
```
Mentions: Monoid.IsTorsionFree, Kaplansky.IsTrivialUnit