Structures · Algebra
DivisionCommMonoid
Commutative DivisionMonoid.
This is the immediate common ancestor of CommGroup and CommGroupWithZero.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_comm
Extends2
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances10
- NonemptyInterval
- DomMulAct
- Interval
- Prod
- OrderDual
- MulOpposite
- Lex
- Colex
- Multiplicative
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by100
- div_eq_inv_mul
- div_pow
- div_div
- div_mul_eq_mul_div
- mul_inv
- inv_mul_eq_div
- div_mul_div_comm
- mul_div_right_comm
- div_right_comm
- mul_comm_div
- Finset.prod_inv_distrib
- mul_zpow
- zpowGroupHom
- mul_div_mul_comm
- div_mul_eq_div_div
- Finset.prod_div_distrib
- div_mul_comm
- invMonoidHom
- div_mul_eq_div_mul_one_div
- IsUnit.mul_div_cancel
- MulEquiv.inv
- mul_div_left_comm
- zpowGroupHom_apply
- div_mul
- one_div_mul_eq_div
- one_div_mul_one_div
- div_zpow
- IsUnit.mul_div_cancel_left
- IsUnit.div_eq_div_iff
- inv_div'
- div_div_div_comm
- finprod_inv_distrib
- divMonoidHom
- IsUnit.div_mul_cancel_left
- IsPrimitiveRoot.inv
- Multiset.prod_map_div
- Finsupp.prod_zpow
- Multiset.prod_map_inv
- inv_div_inv
- AddChar.inv_apply'
- IsUnit.mul_inv_eq_mul_inv_iff
- IsPrimitiveRoot.zpow_eq_one
- AddChar.neg_apply'
- Multiset.prod_map_zpow
- AddChar.zsmul_apply
- inv_mul'
- finprod_div_distrib
- IsPrimitiveRoot.zpow_eq_one_iff_dvd
- div_div_div_eq
- IsUnit.div_div_cancel_left