Structures · Algebra
IsMulTorsionFree
A monoid is torsion-free if power by every non-zero element n : ℕ is injective.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds pow_left_injective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances8
- Nat
- Localization
- FreeGroup
- Subtype
- Prod
- MulOpposite
- HasQuotient.Quotient
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- IsLeftRegular.pow_injective
- not_isOfFinOrder_of_isMulTorsionFree
- pow_left_injective
- pow_eq_one_iff_left
- zpow_left_inj
- pow_left_inj
- MonoidHom.map_neg
- IsMulTorsionFree.pow_left_injective
- self_eq_inv
- IsMulTorsionFree.pow_right_injective₀
- Monoid.minOrder_eq_top
- not_isMulTorsion_of_isMulTorsionFree
- inv_eq_self
- sq_eq_one
- IsMulTorsionFree.pow_right_injective
- MonoidHom.map_sub_swap
- IsOfFinOrder.eq_one'
- isOfFinOrder_iff_eq_one
- zpow_left_injective
- MonoidHom.map_neg_one
- pow_eq_one_iff_right
- Pi.instIsMulTorsionFree
- zpow_eq_zpow_iff'
- IsMulTorsionFree.zpow_eq_one_iff
- IsRightRegular.pow_injective
- self_ne_inv
- Localization.instIsMulTorsionFree
- UniqueFactorizationMonoid.instIsMulTorsionFree
- Subgroup.instIsMulTorsionFree
- IsMulTorsionFree.pow_right_inj
- IsMulTorsionFree.pow_right_inj₀
- AffineMonoid.to_twoUniqueProds
- cauchy_davenport_of_isMulTorsionFree
- AddOpposite.instMulTorsionFree
- not_isTorsion_of_isMulTorsionFree
- IsMulTorsionFree.zpow_eq_one_iff_left
- instIsAddTorsionFreeAdditiveOfIsMulTorsionFree
- Function.Injective.isMulTorsionFree
- pow_eq_one_iff
- IsMulTorsionFree.zpow_eq_one_iff_right
- Prod.instIsMulTorsionFree
- IsMulTorsionFree.orderOf_le_one
- inv_ne_self
Ancestors0
No ancestors.