Theorems · Definition · group theory
IsMulTorsion
(G : Type u_1) → [Monoid G] → Prop
A predicate on a monoid saying that all elements are of finite order.
- Defined in
- Mathlib.GroupTheory.Torsion
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- IsOfFinOrderproof · cited by 113
Cited by40
Results whose statement or proof uses this declaration.
- IsMulTorsion.torsionMulEquivstatement and proof · cited by 4
- IsMulTorsion.torsion_eq_topstatement and proof · cited by 3
- ExponentExists.isMulTorsionstatement · cited by 2
- not_isMulTorsionFree_of_isMulTorsionstatement and proof · cited by 2
- IsMulTorsion.extension_closedstatement and proof · cited by 2
- IsMulTorsion.of_surjectivestatement and proof · cited by 2
- CommGroup.finite_of_fg_isMulTorsionstatement and proof · cited by 2
- isMulTorsion_of_finitestatement · cited by 2
- CommGroup.isMulTorsion_quotient_range_powMonoidHomstatement · cited by 2
- not_isMulTorsion_iffstatement · cited by 1
- not_isMulTorsion_of_isMulTorsionFreestatement and proof · cited by 1
- IsMulTorsion.exponentExistsstatement and proof · cited by 1