Structures · Algebra
LeftCancelMonoid
A monoid in which multiplication is left-cancellative.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by2
Concrete types that are instances9
- DomMulAct
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- Colex
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- orderOf_pos
- isOfFinOrder_of_finite
- orderOf_pow
- pow_eq_pow_iff_modEq
- LeftCancelMonoid.eq_one_of_mul_right
- LeftCancelMonoid.eq_one_of_mul_left
- Monoid.exponent_ne_zero_of_finite
- Monoid.ExponentExists.of_finite
- powersEquivPowers
- infinite_not_isOfFinOrder
- finite_powers
- infinite_powers
- LeftCancelMonoid.mul_eq_one
- Nat.card_submonoidPowers
- LeftCancelMonoid.mul_ne_one
- pow_inj_mod
- injective_pow_iff_not_isOfFinOrder
- instFiniteMonoidHomUnits
- powersEquivPowers_apply
- Monoid.neZero_exponent_of_finite
- Pi.leftCancelMonoid
- LeftCancelMonoid.groupOfFinite
- OrderDual.instLeftCancelMonoid
- Lex.instLeftCancelMonoid
- submonoidOfIdempotent
- Colex.instLeftCancelMonoid
- MonoidHom.instMonoidHomClassMulHom
- mem_powers_iff_mem_range_orderOf
- Monoid.one_lt_exponent
- Function.Injective.leftCancelMonoid
- List.eq_of_prod_take_eq
- MulOpposite.instRightCancelMonoid
- pow_inj_iff_of_orderOf_eq_zero
- FunLike.leftCancelMonoid
- ULift.leftCancelMonoid
- orderOf_eq_card_powers
- Additive.addLeftCancelMonoid
- LeftCancelMonoid.toMonoid
- Prod.instLeftCancelMonoid
- LeftCancelMonoid.to_faithfulSMul_mulOpposite
- LeftCancelMonoid.toIsLeftCancelMul
- LeftCancelMonoid.toLeftCancelSemigroup
- DomMulAct.instLeftCancelMonoidOfMulOpposite