Structures · Algebra
DivInvOneMonoid
A DivInvMonoid where 1⁻¹ = 1.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds inv_one
Extends2
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances4
- ENNReal
- DomMulAct
- EReal
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- div_one
- one_div_one
- DivInvOneMonoid.toDivInvMonoid
- FunLike.divInvOneMonoid
- Function.Injective.divInvOneMonoid
- Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst
- Pi.divInvOneMonoid
- DivInvOneMonoid.toInvOneClass
- DomMulAct.instDivInvOneMonoidOfMulOpposite
- WithZero.instDivInvOneMonoid
- DivInvOneMonoid.inv_one
- Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst'