FormalConjecturesForMathlib/GroupTheory/Torsion.lean

GitHub source file

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

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

6 declarations, 0 contain sorry, 0 declared as axioms

Torsion-free monoids

This file defines Monoid.IsTorsionFree G, the predicate saying that 1 is the only element of finite order in G.

Mathlib's IsMulTorsionFree G asks instead that a ↦ a ^ n be injective for every n ≠ 0 (uniqueness of roots). The two notions agree for commutative groups (isMulTorsionFree_iff_not_isOfFinOrder), but for noncommutative groups IsMulTorsionFree is strictly stronger: the Klein bottle group ⟨a, b | b⁻¹ab = a⁻¹⟩ is torsion-free, yet (ab)² = b² with ab ≠ b. Statements about torsion-free groups in the literature, such as Kaplansky's conjectures on group rings, use the weaker notion defined here.

TODO(mo271): refactor after https://github.com/leanprover-community/mathlib4/pull/43727 lands

Imports (1)
Imported by 1 file
  1. def Monoid.IsTorsionFree A predicate on an additive monoid saying that only 0 has finite order line 42 source

    Source documentation

    A predicate on an additive monoid saying that only 0 has finite order.

    no axioms what this means

    Statement uses: Monoid

    Proof uses: Ne, OfNat.ofNat, Not, IsOfFinOrder

    4 instances, coercions and auxiliary constants left out.

    def Monoid.IsTorsionFree (G : Type*) [Monoid G] : Prop :=
…
  2. theorem Monoid.IsTorsionFree.eq_one_of_isOfFinOrder line 50 source

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

    Statement uses: Monoid, Monoid.IsTorsionFree, IsOfFinOrder, Eq, OfNat.ofNat

    Proof uses: by_contra, Not

    8 instances, coercions and auxiliary constants left out.

  3. theorem Monoid.IsTorsionFree.isOfFinOrder_iff_eq_one line 55 source

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

    Statement uses: Monoid, Monoid.IsTorsionFree, Iff, IsOfFinOrder, Eq, OfNat.ofNat

    Proof uses: Iff.intro, Monoid.IsTorsionFree.eq_one_of_isOfFinOrder, Eq.rec, IsOfFinOrder.one, Eq.symm

    8 instances, coercions and auxiliary constants left out.

  4. theorem Monoid.isTorsionFree_iff_forall_isOfFinOrder_imp_eq_one line 62 source

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

    Statement uses: Monoid, Iff, Monoid.IsTorsionFree, IsOfFinOrder, Eq, OfNat.ofNat

    Proof uses: Iff.intro, Monoid.IsTorsionFree.eq_one_of_isOfFinOrder, Ne

    8 instances, coercions and auxiliary constants left out.

  5. theorem Monoid.IsTorsionFree.of_isMulTorsionFree Uniqueness of roots implies torsion-freeness line 68 source

    Source documentation

    Uniqueness of roots implies torsion-freeness.

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

    Statement uses: Monoid, IsMulTorsionFree, Monoid.IsTorsionFree

    Proof uses: Ne, OfNat.ofNat, not_isOfFinOrder_of_isMulTorsionFree

    4 instances, coercions and auxiliary constants left out.

    theorem Monoid.IsTorsionFree.of_isMulTorsionFree [Monoid G] [IsMulTorsionFree G] :
    Monoid.IsTorsionFree G :=
…

    Mentions: Monoid.IsTorsionFree

  6. theorem Monoid.isTorsionFree_iff_isMulTorsionFree line 75 source

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

    Statement uses: CommGroup, Iff, Monoid.IsTorsionFree, IsMulTorsionFree

    Proof uses: Iff.symm, Ne, OfNat.ofNat, Not, IsOfFinOrder, isMulTorsionFree_iff_not_isOfFinOrder

    12 instances, coercions and auxiliary constants left out.