Structures · Algebra
RightCancelMonoid
A monoid in which multiplication is right-cancellative.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
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 by29
- RightCancelMonoid.pow_eq_pow_iff_modEq
- RightCancelMonoid.eq_one_of_mul_right
- RightCancelMonoid.injective_pow_iff_not_isOfFinOrder
- RightCancelMonoid.eq_one_of_mul_left
- RightCancelMonoid.infinite_powers
- RightCancelMonoid.finite_powers
- Colex.instRightCancelMonoid
- RightCancelMonoid.Nat.card_submonoidPowers
- RightCancelMonoid.infinite_not_isOfFinOrder
- RightCancelMonoid.faithfulSMul
- RightCancelMonoid.mul_eq_one
- RightCancelMonoid.pow_inj_iff_of_orderOf_eq_zero
- MulOpposite.instLeftCancelMonoid
- ULift.rightCancelMonoid
- Prod.instRightCancelMonoid
- Lex.instRightCancelMonoid
- OrderDual.instRightCancelMonoid
- MonoidHom.instMonoidHomClassMulHom_1
- RightCancelMonoid.toMonoid
- FunLike.rightCancelMonoid
- Pi.rightCancelMonoid
- RightCancelMonoid.groupOfFinite
- Function.Injective.rightCancelMonoid
- RightCancelMonoid.toRightCancelSemigroup
- DomMulAct.instRightCancelMonoidOfMulOpposite
- RightCancelMonoid.mul_ne_one
- RightCancelMonoid.pow_inj_mod
- RightCancelMonoid.toIsRightCancelMul
- Additive.addRightCancelMonoid