Structures · Algebra
IsCancelMul
A mixin for cancellative multiplication.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances13
- Filter.Germ
- DomMulAct
- Localization
- OneHom
- Subtype
- Prod
- OrderDual
- MulOpposite
- Lex
- Shrink
- Colex
- Multiplicative
- MonoidHom
How is a type an instance?
Loading the hierarchy index…
Assumed by45
- Function.Injective.isCancelMul
- ThreeGPFree.smul_set
- Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd
- mul_comm_of_exponent_two
- Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
- Commute.of_orderOf_dvd_two
- Set.natCard_mul_le
- threeGPFree_smul_set
- Set.MulAntidiagonal.finite_of_isPWO
- Set.MulAntidiagonal.eq_of_fst_eq_fst
- mulLeftEmbedding_eq_mulRightEmbedding
- threeGPFree_insert
- Localization.decidableEq
- FunLike.isCancelMul
- Equiv.isCancelMul
- commMonoidOfExponentTwo
- ThreeGPFree.eq_right
- IsCancelMul.toIsLeftCancelMul
- IsRegular.all
- Filter.Germ.instIsCancelMul
- Submonoid.LocalizationMap.instIsCancelMulLocalization
- MulOpposite.instIsCancelMul
- Localization.mk_left_injective
- Algebra.GrothendieckGroup.of_injective
- Submonoid.LocalizationMap.instNontrivialLocalizationOfIsCancelMul
- cauchy_davenport_mul_of_linearOrder_isCancelMul
- Submonoid.fg_eqLocusM
- Pi.instIsCancelMul
- MonoidAlgebra.coeff_mul_single_mul
- MulMemClass.isCancelMul
- instIsCancelMulOneHom
- Colex.instIsCancelMul
- IsCancelMul.toIsRightCancelMul
- Additive.isCancelAdd
- MonoidAlgebra.coeff_single_mul_mul
- UniqueProds.of_same
- Prod.instIsCancelMul
- Shrink.instIsCancelMul
- Submonoid.LocalizationMap.isCancelMul
- Set.MulAntidiagonal.eq_of_snd_eq_snd
- OrderDual.instIsCancelMul
- Lex.instIsCancelMul
- DomMulAct.instIsCancelMulOfMulOpposite
- Localization.mk_eq_mk_iff'
- instIsCancelMulMonoidHom