Torsion groups

This file defines torsion groups, i.e. groups where all elements have finite order.

Main definitions

• Monoid.IsTorsion a predicate asserting G is torsion, i.e. that all elements are of finite order.
• CommGroup.torsion G, the torsion subgroup of an abelian group G
• CommMonoid.torsion G, the above stated for commutative monoids
• Monoid.IsTorsionFree, asserting no nontrivial elements have finite order in G
• AddMonoid.IsTorsion and AddMonoid.IsTorsionFree the additive versions of the above

Implementation

All torsion monoids are really groups (which is proven here as Monoid.IsTorsion.group), but since the definition can be stated on monoids it is implemented on Monoid to match other declarations in the group theory library.

Tags

periodic group, aperiodic group, torsion subgroup, torsion abelian group

Future work

• generalize to π-torsion(-free) groups for a set of primes π
• free, free solvable and free abelian groups are torsion free
• complete direct and free products of torsion free groups are torsion free
• groups which are residually finite p-groups with respect to 2 distinct primes are torsion free

def IsMulTorsion (G : Type u_1) [Monoid G] : Prop

A predicate on a monoid saying that all elements are of finite order.

Equations

• IsMulTorsion G = ∀ (g : G), IsOfFinOrder g

def IsAddTorsion (G : Type u_1) [AddMonoid G] : Prop

A predicate on an additive monoid saying that all elements are of finite order.

Equations

• IsAddTorsion G = ∀ (g : G), IsOfFinAddOrder g

@[deprecated IsMulTorsion (since := "2026-07-01")]

def Monoid.IsTorsion (G : Type u_1) [Monoid G] : Prop

Alias of IsMulTorsion.

---

A predicate on a monoid saying that all elements are of finite order.

Equations

• Monoid.IsTorsion = IsMulTorsion

@[deprecated IsAddTorsion (since := "2026-07-01")]

def AddMonoid.IsTorsion (G : Type u_1) [AddMonoid G] : Prop

Alias of IsAddTorsion.

---

A predicate on an additive monoid saying that all elements are of finite order.

Equations

• AddMonoid.IsTorsion = IsAddTorsion

@[simp]

theorem not_isMulTorsion_iff (G : Type u_1) [Monoid G] : ¬IsMulTorsion G ↔ ∃ (g : G), ¬IsOfFinOrder g

A monoid is not a torsion monoid if it has an element of infinite order.

@[simp]

theorem not_isAddTorsion_iff (G : Type u_1) [AddMonoid G] : ¬IsAddTorsion G ↔ ∃ (g : G), ¬IsOfFinAddOrder g

An additive monoid is not a torsion additive monoid if it has an element of infinite order.

@[deprecated not_isMulTorsion_iff (since := "2026-07-01")]

theorem Monoid.not_isTorsion_iff (G : Type u_1) [Monoid G] : ¬IsMulTorsion G ↔ ∃ (g : G), ¬IsOfFinOrder g

Alias of not_isMulTorsion_iff.

---

A monoid is not a torsion monoid if it has an element of infinite order.

@[deprecated not_isAddTorsion_iff (since := "2026-07-01")]

theorem AddMonoid.not_isTorsion_iff (G : Type u_1) [AddMonoid G] : ¬IsAddTorsion G ↔ ∃ (g : G), ¬IsOfFinAddOrder g

Alias of not_isAddTorsion_iff.

---

An additive monoid is not a torsion additive monoid if it has an element of infinite order.

@[instance_reducible]

noncomputable def IsMulTorsion.group {G : Type u_1} [Monoid G] (tG : IsMulTorsion G) : Group G

Torsion monoids are really groups.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def IsAddTorsion.addGroup {G : Type u_1} [AddMonoid G] (tG : IsAddTorsion G) : AddGroup G

Torsion additive monoids are really additive groups.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated IsMulTorsion.group (since := "2026-07-01")]

def IsTorsion.group {G : Type u_1} [Monoid G] (tG : IsMulTorsion G) : Group G

Alias of IsMulTorsion.group.

---

Torsion monoids are really groups.

Equations

• @IsTorsion.group = @IsMulTorsion.group

@[deprecated IsAddTorsion.addGroup (since := "2026-07-01")]

def IsTorsion.addGroup {G : Type u_1} [AddMonoid G] (tG : IsAddTorsion G) : AddGroup G

Alias of IsAddTorsion.addGroup.

---

Torsion additive monoids are really additive groups.

Equations

• @IsTorsion.addGroup = @IsAddTorsion.addGroup

theorem IsMulTorsion.subgroup {G : Type u_1} [Group G] (tG : IsMulTorsion G) (H : Subgroup G) : IsMulTorsion ↥H

Subgroups of torsion groups are torsion groups.

theorem IsAddTorsion.addSubgroup {G : Type u_1} [AddGroup G] (tG : IsAddTorsion G) (H : AddSubgroup G) : IsAddTorsion ↥H

Additive subgroups of torsion additive groups are torsion additive groups.

@[deprecated IsMulTorsion.subgroup (since := "2026-07-01")]

theorem IsTorsion.subgroup {G : Type u_1} [Group G] (tG : IsMulTorsion G) (H : Subgroup G) : IsMulTorsion ↥H

Alias of IsMulTorsion.subgroup.

---

Subgroups of torsion groups are torsion groups.

@[deprecated IsAddTorsion.addSubgroup (since := "2026-07-01")]

theorem IsTorsion.addSubgroup {G : Type u_1} [AddGroup G] (tG : IsAddTorsion G) (H : AddSubgroup G) : IsAddTorsion ↥H

Alias of IsAddTorsion.addSubgroup.

---

Additive subgroups of torsion additive groups are torsion additive groups.

theorem IsMulTorsion.of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (tG : IsMulTorsion G) : IsMulTorsion H

The image of a surjective torsion group homomorphism is torsion.

theorem IsAddTorsion.of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (tG : IsAddTorsion G) : IsAddTorsion H

The image of a surjective torsion additive group homomorphism is torsion.

@[deprecated IsMulTorsion.of_surjective (since := "2026-06-30")]

theorem IsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (tG : IsMulTorsion G) : IsMulTorsion H

Alias of IsMulTorsion.of_surjective.

---

The image of a surjective torsion group homomorphism is torsion.

@[deprecated IsAddTorsion.of_surjective (since := "2026-06-30")]

theorem AddIsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (tG : IsAddTorsion G) : IsAddTorsion H

Alias of IsAddTorsion.of_surjective.

---

The image of a surjective torsion additive group homomorphism is torsion.

theorem IsMulTorsion.extension_closed {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hN : N = f.ker) (tH : IsMulTorsion H) (tN : IsMulTorsion ↥N) : IsMulTorsion G

Torsion groups are closed under extensions.

theorem IsAddTorsion.extension_closed {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hN : N = f.ker) (tH : IsAddTorsion H) (tN : IsAddTorsion ↥N) : IsAddTorsion G

Torsion additive groups are closed under extensions.

@[deprecated IsMulTorsion.extension_closed (since := "2026-06-30")]

theorem IsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hN : N = f.ker) (tH : IsMulTorsion H) (tN : IsMulTorsion ↥N) : IsMulTorsion G

Alias of IsMulTorsion.extension_closed.

---

Torsion groups are closed under extensions.

@[deprecated IsAddTorsion.extension_closed (since := "2026-06-30")]

theorem AddIsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hN : N = f.ker) (tH : IsAddTorsion H) (tN : IsAddTorsion ↥N) : IsAddTorsion G

Alias of IsAddTorsion.extension_closed.

---

Torsion additive groups are closed under extensions.

theorem IsMulTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (hN : N = f.ker) (tN : IsMulTorsion ↥N) : IsMulTorsion H ↔ IsMulTorsion G

The image of a quotient is torsion iff the group is torsion.

theorem IsAddTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (hN : N = f.ker) (tN : IsAddTorsion ↥N) : IsAddTorsion H ↔ IsAddTorsion G

The image of a quotient is torsion iff the additive group is torsion.

@[deprecated IsMulTorsion.quotient_iff (since := "2026-06-30")]

theorem IsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (hN : N = f.ker) (tN : IsMulTorsion ↥N) : IsMulTorsion H ↔ IsMulTorsion G

Alias of IsMulTorsion.quotient_iff.

---

The image of a quotient is torsion iff the group is torsion.

@[deprecated IsAddTorsion.quotient_iff (since := "2026-06-30")]

theorem AddIsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (hN : N = f.ker) (tN : IsAddTorsion ↥N) : IsAddTorsion H ↔ IsAddTorsion G

Alias of IsAddTorsion.quotient_iff.

---

The image of a quotient is torsion iff the additive group is torsion.

theorem ExponentExists.isMulTorsion {G : Type u_1} [Group G] (h : Monoid.ExponentExists G) : IsMulTorsion G

If a group exponent exists, the group is torsion.

theorem ExponentExists.isAddTorsion {G : Type u_1} [AddGroup G] (h : AddMonoid.ExponentExists G) : IsAddTorsion G

If a group exponent exists, the additive group is torsion.

@[deprecated ExponentExists.isMulTorsion (since := "2026-06-30")]

theorem ExponentExists.isTorsion {G : Type u_1} [Group G] (h : Monoid.ExponentExists G) : IsMulTorsion G

Alias of ExponentExists.isMulTorsion.

---

If a group exponent exists, the group is torsion.

@[deprecated ExponentExists.isAddTorsion (since := "2026-06-30")]

theorem ExponentExists.is_add_torsion {G : Type u_1} [AddGroup G] (h : AddMonoid.ExponentExists G) : IsAddTorsion G

Alias of ExponentExists.isAddTorsion.

---

If a group exponent exists, the additive group is torsion.

theorem IsMulTorsion.exponentExists {G : Type u_1} [Group G] (tG : IsMulTorsion G) (bounded : (Set.range fun (g : G) => orderOf g).Finite) : Monoid.ExponentExists G

The group exponent exists for any bounded torsion group.

theorem IsAddTorsion.exponentExists {G : Type u_1} [AddGroup G] (tG : IsAddTorsion G) (bounded : (Set.range fun (g : G) => addOrderOf g).Finite) : AddMonoid.ExponentExists G

The group exponent exists for any bounded torsion additive group.

@[deprecated IsMulTorsion.exponentExists (since := "2026-07-01")]

theorem IsTorsion.exponentExists {G : Type u_1} [Group G] (tG : IsMulTorsion G) (bounded : (Set.range fun (g : G) => orderOf g).Finite) : Monoid.ExponentExists G

Alias of IsMulTorsion.exponentExists.

---

The group exponent exists for any bounded torsion group.

theorem isMulTorsion_of_finite {G : Type u_1} [Group G] [Finite G] : IsMulTorsion G

Finite groups are torsion groups.

theorem isAddTorsion_of_finite {G : Type u_1} [AddGroup G] [Finite G] : IsAddTorsion G

Finite additive groups are torsion additive groups.

@[deprecated isMulTorsion_of_finite (since := "2026-06-30")]

theorem isTorsion_of_finite {G : Type u_1} [Group G] [Finite G] : IsMulTorsion G

Alias of isMulTorsion_of_finite.

---

Finite groups are torsion groups.

@[deprecated isAddTorsion_of_finite (since := "2026-06-30")]

theorem is_add_torsion_of_finite {G : Type u_1} [AddGroup G] [Finite G] : IsAddTorsion G

Alias of isAddTorsion_of_finite.

---

Finite additive groups are torsion additive groups.

theorem not_isMulTorsionFree_of_isMulTorsion {G : Type u_1} [CommGroup G] [Nontrivial G] (hG : IsMulTorsion G) : ¬IsMulTorsionFree G

A nontrivial torsion abelian group is not torsion-free.

theorem not_isAddTorsionFree_of_isAddTorsion {G : Type u_1} [AddCommGroup G] [Nontrivial G] (hG : IsAddTorsion G) : ¬IsAddTorsionFree G

A nontrivial torsion additive abelian group is not torsion-free.

@[deprecated not_isMulTorsionFree_of_isMulTorsion (since := "2026-07-01")]

theorem not_isMulTorsionFree_of_isTorsion {G : Type u_1} [CommGroup G] [Nontrivial G] (hG : IsMulTorsion G) : ¬IsMulTorsionFree G

Alias of not_isMulTorsionFree_of_isMulTorsion.

---

A nontrivial torsion abelian group is not torsion-free.

@[deprecated not_isAddTorsionFree_of_isAddTorsion (since := "2026-07-01")]

theorem not_isAddTorsionFree_of_isTorsion {G : Type u_1} [AddCommGroup G] [Nontrivial G] (hG : IsAddTorsion G) : ¬IsAddTorsionFree G

Alias of not_isAddTorsionFree_of_isAddTorsion.

---

A nontrivial torsion additive abelian group is not torsion-free.

theorem not_isMulTorsion_of_isMulTorsionFree {G : Type u_1} [CommGroup G] [Nontrivial G] [IsMulTorsionFree G] : ¬IsMulTorsion G

A nontrivial torsion-free abelian group is not torsion.

theorem not_isAddTorsion_of_isAddTorsionFree {G : Type u_1} [AddCommGroup G] [Nontrivial G] [IsAddTorsionFree G] : ¬IsAddTorsion G

A nontrivial torsion-free additive abelian group is not torsion.

@[deprecated not_isMulTorsion_of_isMulTorsionFree (since := "2026-07-01")]

theorem not_isTorsion_of_isMulTorsionFree {G : Type u_1} [CommGroup G] [Nontrivial G] [IsMulTorsionFree G] : ¬IsMulTorsion G

Alias of not_isMulTorsion_of_isMulTorsionFree.

---

A nontrivial torsion-free abelian group is not torsion.

@[deprecated not_isAddTorsion_of_isAddTorsionFree (since := "2026-07-01")]

theorem not_isTorsion_of_isAddTorsionFree {G : Type u_1} [AddCommGroup G] [Nontrivial G] [IsAddTorsionFree G] : ¬IsAddTorsion G

Alias of not_isAddTorsion_of_isAddTorsionFree.

---

A nontrivial torsion-free additive abelian group is not torsion.

theorem IsAddTorsion.module_of_torsion (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] (tR : IsAddTorsion R) : IsAddTorsion M

A module whose scalars are torsion is torsion.

@[deprecated IsAddTorsion.module_of_torsion (since := "2026-07-01")]

theorem AddMonoid.IsTorsion.module_of_torsion (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] (tR : IsAddTorsion R) : IsAddTorsion M

Alias of IsAddTorsion.module_of_torsion.

---

A module whose scalars are torsion is torsion.

theorem IsAddTorsion.module_of_finite (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Ring R] [Finite R] [Module R M] : IsAddTorsion M

A module with a finite ring of scalars is torsion.

@[deprecated IsAddTorsion.module_of_finite (since := "2026-07-01")]

theorem AddMonoid.IsTorsion.module_of_finite (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Ring R] [Finite R] [Module R M] : IsAddTorsion M

Alias of IsAddTorsion.module_of_finite.

---

A module with a finite ring of scalars is torsion.

def CommMonoid.torsion (G : Type u_1) [CommMonoid G] : Submonoid G

The torsion submonoid of a commutative monoid.

(Note that by IsMulTorsion.group torsion monoids are truthfully groups.)

Equations

• CommMonoid.torsion G = { carrier := {x : G | IsOfFinOrder x}, mul_mem' := ⋯, one_mem' := ⋯ }

def AddCommMonoid.addTorsion (G : Type u_1) [AddCommMonoid G] : AddSubmonoid G

The torsion additive submonoid of an additive commutative monoid.

Equations

• AddCommMonoid.addTorsion G = { carrier := {x : G | IsOfFinAddOrder x}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem CommMonoid.mem_torsion (G : Type u_1) [CommMonoid G] (g : G) : g ∈ torsion G ↔ IsOfFinOrder g

theorem AddCommMonoid.mem_torsion (G : Type u_1) [AddCommMonoid G] (g : G) : g ∈ addTorsion G ↔ IsOfFinAddOrder g

theorem CommMonoid.torsion_prod (G : Type u_1) {H : Type u_2} [CommMonoid G] [CommMonoid H] : torsion (G × H) = (torsion G).prod (torsion H)

theorem AddCommMonoid.torsion_sum (G : Type u_1) {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] : addTorsion (G × H) = (addTorsion G).prod (addTorsion H)

theorem CommMonoid.torsion.isMulTorsion {G : Type u_1} [CommMonoid G] : IsMulTorsion ↥(torsion G)

Torsion submonoids are torsion.

theorem AddCommMonoid.addTorsion.isAddTorsion {G : Type u_1} [AddCommMonoid G] : IsAddTorsion ↥(addTorsion G)

Torsion additive submonoids are torsion.

@[deprecated CommMonoid.torsion.isMulTorsion (since := "2026-07-01")]

theorem CommMonoid.torsion.isTorsion {G : Type u_1} [CommMonoid G] : IsMulTorsion ↥(torsion G)

Alias of CommMonoid.torsion.isMulTorsion.

---

Torsion submonoids are torsion.

@[deprecated AddCommMonoid.addTorsion.isAddTorsion (since := "2026-07-01")]

theorem AddCommMonoid.addTorsion.isTorsion {G : Type u_1} [AddCommMonoid G] : IsAddTorsion ↥(addTorsion G)

Alias of AddCommMonoid.addTorsion.isAddTorsion.

---

Torsion additive submonoids are torsion.

def CommMonoid.primaryComponent (G : Type u_1) [CommMonoid G] (p : ℕ) : Submonoid G

The p-primary component is the submonoid of elements g such that g ^ p ^ k = 1 for some k. For prime p, these are exactly the elements of p-power order.

Equations

• CommMonoid.primaryComponent G p = { carrier := {g : G | ∃ (k : ℕ), g ^ p ^ k = 1}, mul_mem' := ⋯, one_mem' := ⋯ }

def AddCommMonoid.primaryComponent (G : Type u_1) [AddCommMonoid G] (p : ℕ) : AddSubmonoid G

The additive p-primary component is the submonoid of elements g such that p ^ k • g = 0 for some k. For prime p, these are exactly the elements of additive p-power order.

Equations

• AddCommMonoid.primaryComponent G p = { carrier := {g : G | ∃ (k : ℕ), p ^ k • g = 0}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem CommMonoid.mem_primaryComponent {G : Type u_1} [CommMonoid G] {p : ℕ} {g : G} : g ∈ primaryComponent G p ↔ ∃ (k : ℕ), g ^ p ^ k = 1

g lies in the p-primary component iff g ^ p ^ k = 1 for some k.

@[simp]

theorem AddCommMonoid.mem_primaryComponent {G : Type u_1} [AddCommMonoid G] {p : ℕ} {g : G} : g ∈ primaryComponent G p ↔ ∃ (k : ℕ), p ^ k • g = 0

g lies in the additive p-primary component iff p ^ k • g = 0 for some k.

theorem CommMonoid.mem_primaryComponent_iff_orderOf {G : Type u_1} [CommMonoid G] {p : ℕ} [Fact (Nat.Prime p)] {g : G} : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), orderOf g = p ^ n

For prime p, g lies in the p-primary component iff its order is a power of p.

theorem AddCommMonoid.mem_primaryComponent_iff_addOrderOf {G : Type u_1} [AddCommMonoid G] {p : ℕ} [Fact (Nat.Prime p)] {g : G} : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), addOrderOf g = p ^ n

For prime p, g lies in the additive p-primary component iff its additive order is a power of p.

theorem CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow {G : Type u_1} [CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(primaryComponent G p)) : ∃ (n : ℕ), orderOf g = p ^ n

Elements of the p-primary component have order p^n for some n.

theorem AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul {G : Type u_1} [AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(primaryComponent G p)) : ∃ (n : ℕ), addOrderOf g = p ^ n

Elements of the p-primary component have additive order p^n for some n.

theorem CommMonoid.primaryComponent.disjoint {G : Type u_1} [CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')] (hne : p ≠ p') : Disjoint (primaryComponent G p) (primaryComponent G p')

The p- and q-primary components are disjoint for p ≠ q.

theorem AddCommMonoid.primaryComponent.disjoint {G : Type u_1} [AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')] (hne : p ≠ p') : Disjoint (primaryComponent G p) (primaryComponent G p')

The p- and q-primary components are disjoint for p ≠ q.

@[simp]

theorem IsMulTorsion.torsion_eq_top {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) : CommMonoid.torsion G = ⊤

The torsion submonoid of a torsion monoid is ⊤.

@[simp]

theorem IsAddTorsion.torsion_eq_top {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) : AddCommMonoid.addTorsion G = ⊤

The torsion additive submonoid of a torsion additive monoid is ⊤.

def IsMulTorsion.torsionMulEquiv {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) : ↥(CommMonoid.torsion G) ≃* G

A torsion monoid is isomorphic to its torsion submonoid.

Equations

• tG.torsionMulEquiv = (MulEquiv.submonoidCongr ⋯).trans Submonoid.topEquiv

def IsAddTorsion.torsionAddEquiv {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) : ↥(AddCommMonoid.addTorsion G) ≃+ G

A torsion additive monoid is isomorphic to its torsion additive submonoid.

Equations

• tG.torsionAddEquiv = (AddEquiv.addSubmonoidCongr ⋯).trans AddSubmonoid.topEquiv

@[simp]

theorem IsMulTorsion.torsionMulEquiv_symm_apply_coe {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) (a✝ : G) : ↑(tG.torsionMulEquiv.symm a✝) = a✝

@[simp]

theorem IsAddTorsion.torsionAddEquiv_symm_apply_coe {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) (a✝ : G) : ↑(tG.torsionAddEquiv.symm a✝) = a✝

@[simp]

theorem IsAddTorsion.torsionAddEquiv_apply {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) (a✝ : ↥(AddCommMonoid.addTorsion G)) : tG.torsionAddEquiv a✝ = ↑((AddEquiv.addSubmonoidCongr ⋯) a✝)

@[simp]

theorem IsMulTorsion.torsionMulEquiv_apply {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) (a✝ : ↥(CommMonoid.torsion G)) : tG.torsionMulEquiv a✝ = ↑((MulEquiv.submonoidCongr ⋯) a✝)

@[deprecated IsMulTorsion.torsion_eq_top (since := "2026-07-01")]

theorem Monoid.IsTorsion.torsion_eq_top {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) : CommMonoid.torsion G = ⊤

Alias of IsMulTorsion.torsion_eq_top.

---

The torsion submonoid of a torsion monoid is ⊤.

@[deprecated IsAddTorsion.torsion_eq_top (since := "2026-07-01")]

theorem AddMonoid.IsTorsion.torsion_eq_top {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) : AddCommMonoid.addTorsion G = ⊤

Alias of IsAddTorsion.torsion_eq_top.

---

The torsion additive submonoid of a torsion additive monoid is ⊤.

@[deprecated IsMulTorsion.torsionMulEquiv (since := "2026-07-01")]

def Monoid.IsTorsion.torsionMulEquiv {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) : ↥(CommMonoid.torsion G) ≃* G

Alias of IsMulTorsion.torsionMulEquiv.

---

A torsion monoid is isomorphic to its torsion submonoid.

Equations

• @Monoid.IsTorsion.torsionMulEquiv = @IsMulTorsion.torsionMulEquiv

@[deprecated IsAddTorsion.torsionAddEquiv (since := "2026-07-01")]

def AddMonoid.IsTorsion.torsionAddEquiv {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) : ↥(AddCommMonoid.addTorsion G) ≃+ G

Alias of IsAddTorsion.torsionAddEquiv.

---

A torsion additive monoid is isomorphic to its torsion additive submonoid.

Equations

• @AddMonoid.IsTorsion.torsionAddEquiv = @IsAddTorsion.torsionAddEquiv

@[deprecated IsMulTorsion.torsionMulEquiv_apply (since := "2026-07-01")]

theorem Monoid.IsTorsion.torsionMulEquiv_apply {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) (a✝ : ↥(CommMonoid.torsion G)) : tG.torsionMulEquiv a✝ = ↑((MulEquiv.submonoidCongr ⋯) a✝)

Alias of IsMulTorsion.torsionMulEquiv_apply.

@[deprecated IsAddTorsion.torsionAddEquiv_apply (since := "2026-07-01")]

theorem AddMonoid.IsTorsion.torsionAddEquiv_apply {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) (a✝ : ↥(AddCommMonoid.addTorsion G)) : tG.torsionAddEquiv a✝ = ↑((AddEquiv.addSubmonoidCongr ⋯) a✝)

Alias of IsAddTorsion.torsionAddEquiv_apply.

@[deprecated IsMulTorsion.torsionMulEquiv_symm_apply_coe (since := "2026-07-01")]

theorem Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe {G : Type u_1} [CommMonoid G] (tG : IsMulTorsion G) (a✝ : G) : ↑(tG.torsionMulEquiv.symm a✝) = a✝

Alias of IsMulTorsion.torsionMulEquiv_symm_apply_coe.

@[deprecated IsAddTorsion.torsionAddEquiv_symm_apply_coe (since := "2026-07-01")]

theorem AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe {G : Type u_1} [AddCommMonoid G] (tG : IsAddTorsion G) (a✝ : G) : ↑(tG.torsionAddEquiv.symm a✝) = a✝

Alias of IsAddTorsion.torsionAddEquiv_symm_apply_coe.

def CommMonoid.Torsion.ofTorsion (G : Type u_1) [CommMonoid G] : ↥(torsion ↥(torsion G)) ≃* ↥(torsion G)

Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.

Equations

• CommMonoid.Torsion.ofTorsion G = ⋯.torsionMulEquiv

def AddCommMonoid.Torsion.ofTorsion (G : Type u_1) [AddCommMonoid G] : ↥(addTorsion ↥(addTorsion G)) ≃+ ↥(addTorsion G)

Torsion additive submonoids of a torsion additive submonoid are isomorphic to the additive submonoid.

Equations

• AddCommMonoid.Torsion.ofTorsion G = ⋯.torsionAddEquiv

@[deprecated CommMonoid.Torsion.ofTorsion (since := "2026-07-01")]

def Torsion.ofTorsion (G : Type u_1) [CommMonoid G] : ↥(CommMonoid.torsion ↥(CommMonoid.torsion G)) ≃* ↥(CommMonoid.torsion G)

Alias of CommMonoid.Torsion.ofTorsion.

---

Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.

Equations

• Torsion.ofTorsion = CommMonoid.Torsion.ofTorsion

def CommGroup.torsion (G : Type u_1) [CommGroup G] : Subgroup G

The torsion subgroup of an abelian group.

Equations

• CommGroup.torsion G = { toSubmonoid := CommMonoid.torsion G, inv_mem' := ⋯ }

def AddCommGroup.torsion (G : Type u_1) [AddCommGroup G] : AddSubgroup G

The torsion additive subgroup of an additive abelian group.

Equations

• AddCommGroup.torsion G = { toAddSubmonoid := AddCommMonoid.addTorsion G, neg_mem' := ⋯ }

theorem CommGroup.torsion_eq_torsion_submonoid (G : Type u_1) [CommGroup G] : CommMonoid.torsion G = (torsion G).toSubmonoid

The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.

theorem AddCommGroup.torsion_eq_torsion_addSubmonoid (G : Type u_1) [AddCommGroup G] : AddCommMonoid.addTorsion G = (torsion G).toAddSubmonoid

The torsion additive submonoid of an abelian group equals the torsion additive subgroup as an additive submonoid.

@[deprecated AddCommGroup.torsion_eq_torsion_addSubmonoid (since := "2026-07-01")]

theorem AddCommGroup.add_torsion_eq_add_torsion_submonoid (G : Type u_1) [AddCommGroup G] : AddCommMonoid.addTorsion G = (torsion G).toAddSubmonoid

Alias of AddCommGroup.torsion_eq_torsion_addSubmonoid.

---

The torsion additive submonoid of an abelian group equals the torsion additive subgroup as an additive submonoid.

theorem CommGroup.mem_torsion {G : Type u_1} [CommGroup G] (g : G) : g ∈ torsion G ↔ IsOfFinOrder g

theorem AddCommGroup.mem_torsion {G : Type u_1} [AddCommGroup G] (g : G) : g ∈ torsion G ↔ IsOfFinAddOrder g

theorem CommGroup.torsion_eq_top_iff {G : Type u_1} [CommGroup G] : torsion G = ⊤ ↔ IsMulTorsion G

theorem AddCommGroup.torsion_eq_top_iff {G : Type u_1} [AddCommGroup G] : torsion G = ⊤ ↔ IsAddTorsion G

theorem CommGroup.isMulTorsionFree_iff_torsion_eq_bot {G : Type u_1} [CommGroup G] : IsMulTorsionFree G ↔ torsion G = ⊥

theorem AddCommGroup.isAddTorsionFree_iff_torsion_eq_bot {G : Type u_1} [AddCommGroup G] : IsAddTorsionFree G ↔ torsion G = ⊥

theorem CommGroup.le_comap_torsion {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (f : G →* H) : torsion G ≤ Subgroup.comap f (torsion H)

theorem AddCommGroup.le_comap_torsion {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] (f : G →+ H) : torsion G ≤ AddSubgroup.comap f (torsion H)

theorem CommGroup.map_torsion_le {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (f : G →* H) : Subgroup.map f (torsion G) ≤ torsion H

theorem AddCommGroup.map_torsion_le {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] (f : G →+ H) : AddSubgroup.map f (torsion G) ≤ torsion H

theorem CommGroup.comap_torsion_of_injective {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] {f : G →* H} (hf : Function.Injective ⇑f) : Subgroup.comap f (torsion H) = torsion G

theorem AddCommGroup.comap_torsion_of_injective {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] {f : G →+ H} (hf : Function.Injective ⇑f) : AddSubgroup.comap f (torsion H) = torsion G

theorem MulEquiv.comap_torsion {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (e : G ≃* H) : Subgroup.comap (↑e) (CommGroup.torsion H) = CommGroup.torsion G

theorem AddEquiv.comap_torsion {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] (e : G ≃+ H) : AddSubgroup.comap (↑e) (AddCommGroup.torsion H) = AddCommGroup.torsion G

theorem MulEquiv.map_torsion {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (e : G ≃* H) : Subgroup.map (↑e) (CommGroup.torsion G) = CommGroup.torsion H

theorem AddEquiv.map_torsion {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] (e : G ≃+ H) : AddSubgroup.map (↑e) (AddCommGroup.torsion G) = AddCommGroup.torsion H

theorem CommGroup.torsion_prod {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] : torsion (G × H) = (torsion G).prod (torsion H)

theorem AddCommGroup.torsion_sum {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] : torsion (G × H) = (torsion G).prod (torsion H)

theorem CommGroup.isMulTorsion_quotient_range_powMonoidHom (G : Type u_1) [CommGroup G] {n : ℕ} (hn : n ≠ 0) : IsMulTorsion (G ⧸ (powMonoidHom n).range)

theorem AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHom (G : Type u_1) [AddCommGroup G] {n : ℕ} (hn : n ≠ 0) : IsAddTorsion (G ⧸ (nsmulAddMonoidHom n).range)

@[deprecated CommGroup.isMulTorsion_quotient_range_powMonoidHom (since := "2026-07-01")]

theorem CommGroup.isTorsion_quotient_range_powMonoidHom (G : Type u_1) [CommGroup G] {n : ℕ} (hn : n ≠ 0) : IsMulTorsion (G ⧸ (powMonoidHom n).range)

Alias of CommGroup.isMulTorsion_quotient_range_powMonoidHom.

@[deprecated AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHom (since := "2026-07-01")]

theorem AddCommGroup.isTorsion_quotient_range_nsmulAddMonoidHom (G : Type u_1) [AddCommGroup G] {n : ℕ} (hn : n ≠ 0) : IsAddTorsion (G ⧸ (nsmulAddMonoidHom n).range)

Alias of AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHom.

def CommGroup.primaryComponent (G : Type u_1) [CommGroup G] (p : ℕ) : Subgroup G

The p-primary component is the subgroup of elements g such that g ^ p ^ k = 1 for some k. For prime p, these are exactly the elements of p-power order.

Equations

• CommGroup.primaryComponent G p = { toSubmonoid := CommMonoid.primaryComponent G p, inv_mem' := ⋯ }

def AddCommGroup.primaryComponent (G : Type u_1) [AddCommGroup G] (p : ℕ) : AddSubgroup G

The additive p-primary component is the subgroup of elements g such that p ^ k • g = 0 for some k. For prime p, these are exactly the elements of additive p-power order.

Equations

• AddCommGroup.primaryComponent G p = { toAddSubmonoid := AddCommMonoid.primaryComponent G p, neg_mem' := ⋯ }

@[simp]

theorem CommGroup.mem_primaryComponent {G : Type u_1} [CommGroup G] {p : ℕ} {g : G} : g ∈ primaryComponent G p ↔ ∃ (k : ℕ), g ^ p ^ k = 1

g lies in the p-primary component iff g ^ p ^ k = 1 for some k.

@[simp]

theorem AddCommGroup.mem_primaryComponent {G : Type u_1} [AddCommGroup G] {p : ℕ} {g : G} : g ∈ primaryComponent G p ↔ ∃ (k : ℕ), p ^ k • g = 0

g lies in the additive p-primary component iff p ^ k • g = 0 for some k.

theorem CommGroup.mem_primaryComponent_iff_orderOf {G : Type u_1} [CommGroup G] {p : ℕ} [Fact (Nat.Prime p)] {g : G} : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), orderOf g = p ^ n

For prime p, g lies in the p-primary component iff its order is a power of p.

theorem AddCommGroup.mem_primaryComponent_iff_addOrderOf {G : Type u_1} [AddCommGroup G] {p : ℕ} [Fact (Nat.Prime p)] {g : G} : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), addOrderOf g = p ^ n

For prime p, g lies in the additive p-primary component iff its additive order is a power of p.

theorem CommGroup.primaryComponent.isPGroup {G : Type u_1} [CommGroup G] {p : ℕ} : IsPGroup p ↥(primaryComponent G p)

The p-primary component is a p-group.

noncomputable def CommGroup.freeRank (G : Type u_1) [CommGroup G] [Group.FG G] : ℕ

The free rank of a finitely generated abelian group is the rank of its free part.

Equations

• CommGroup.freeRank G = Group.rank (G ⧸ CommGroup.torsion G)

noncomputable def AddCommGroup.freeRank (G : Type u_1) [AddCommGroup G] [AddGroup.FG G] : ℕ

The free rank of a finitely generated abelian group is the rank of its free part.

Equations

• AddCommGroup.freeRank G = AddGroup.rank (G ⧸ AddCommGroup.torsion G)

theorem CommGroup.freeRank_def (G : Type u_1) [CommGroup G] [Group.FG G] : freeRank G = Group.rank (G ⧸ torsion G)

theorem AddCommGroup.freeRank_def (G : Type u_1) [AddCommGroup G] [AddGroup.FG G] : freeRank G = AddGroup.rank (G ⧸ torsion G)

theorem CommGroup.freeRank_eq_zero_iff {G : Type u_1} [CommGroup G] [Group.FG G] : freeRank G = 0 ↔ IsMulTorsion G

theorem AddCommGroup.freeRank_eq_zero_iff {G : Type u_1} [AddCommGroup G] [AddGroup.FG G] : freeRank G = 0 ↔ IsAddTorsion G

theorem CommGroup.freeRank_eq_zero {G : Type u_1} [CommGroup G] (hG : IsMulTorsion G) [Group.FG G] : freeRank G = 0

theorem AddCommGroup.freeRank_eq_zero {G : Type u_1} [AddCommGroup G] (hG : IsAddTorsion G) [AddGroup.FG G] : freeRank G = 0

theorem CommGroup.freeRank_eq_zero_of_finite {G : Type u_1} [CommGroup G] [Finite G] : freeRank G = 0

theorem AddCommGroup.freeRank_eq_zero_of_finite {G : Type u_1} [AddCommGroup G] [Finite G] : freeRank G = 0

theorem CommGroup.freeRank_congr {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] [Group.FG G] [Group.FG H] (e : G ≃* H) : freeRank G = freeRank H

theorem AddCommGroup.freeRank_congr {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] [AddGroup.FG G] [AddGroup.FG H] (e : G ≃+ H) : freeRank G = freeRank H

theorem CommGroup.freeRank_ge_of_surjective {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] [Group.FG G] [Group.FG H] (e : G →* H) (he : Function.Surjective ⇑e) : freeRank H ≤ freeRank G

theorem AddCommGroup.freeRank_ge_of_surjective {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] [AddGroup.FG G] [AddGroup.FG H] (e : G →+ H) (he : Function.Surjective ⇑e) : freeRank H ≤ freeRank G

instance QuotientGroup.instIsMulTorsionFree (G : Type u_1) [CommGroup G] : IsMulTorsionFree (G ⧸ CommGroup.torsion G)

Quotienting a group by its torsion subgroup yields a torsion-free group.

instance QuotientAddGroup.instIsAddTorsionFree (G : Type u_1) [AddCommGroup G] : IsAddTorsionFree (G ⧸ AddCommGroup.torsion G)

Quotienting an additive group by its torsion additive subgroup yields a torsion-free additive group.

@[instance_reducible]

instance instModuleQuotientAddSubgroupTorsion {R : Type u_3} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] : Module R (M ⧸ AddCommGroup.torsion M)

Equations

• One or more equations did not get rendered due to their size.

theorem neg_one_mem_torsion {M : Type u_3} [CommMonoid M] [HasDistribNeg M] : -1 ∈ CommMonoid.torsion M