Theorems · Definition · group theory
CommMonoid.torsion
(G : Type u_1) → [inst : CommMonoid G] → Submonoid G
The torsion submonoid of a commutative monoid.
(Note that by IsMulTorsion.group torsion monoids are truthfully groups.)
- Defined in
- Mathlib.GroupTheory.Torsion
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- Submonoidstatement · cited by 3,086
- CommMonoidstatement and proof · cited by 2,264
- IsOfFinOrderproof · cited by 113
- IsOfFinOrder.mulproof · cited by 0
Cited by17
Results whose statement or proof uses this declaration.
- CommGroup.torsionproof · cited by 16
- IsMulTorsion.torsionMulEquivstatement · cited by 4
- IsMulTorsion.torsion_eq_topstatement and proof · cited by 3
- neg_one_mem_torsionstatement · cited by 2
- CommMonoid.torsion.isMulTorsionstatement and proof · cited by 1
- IsMulTorsion.torsionMulEquiv_applystatement and proof · cited by 1
- IsMulTorsion.torsionMulEquiv_symm_apply_coestatement · cited by 1
- Torsion.ofTorsionstatement · cited by 0
- CommMonoid.torsion.isTorsionstatement · cited by 0
- CommMonoid.mem_torsionstatement · cited by 0
- CommGroup.torsion_eq_torsion_submonoidstatement · cited by 0
- CommMonoid.torsion_prodstatement · cited by 0