Structures · Algebra
InvOneClass
Typeclass for expressing that 1⁻¹ = 1.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds inv_one
Extends2
Extended by1
Concrete types that are instances8
- SeparationQuotient
- Filter.Germ
- Matrix
- DomMulAct
- MvPowerSeries
- FractionalIdeal
- WithZero
- WithOne
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- inv_one
- InvOneClass.inv_one
- InvOneClass.toInv
- Pi.invOneClass
- OneHom.inv_comp
- WithZero.invOneClass
- OneHom.coe_inv
- OneHom.inv_apply
- DomMulAct.instInvOneClassOfMulOpposite
- FunLike.invOneClass
- InvOneClass.toOne
- OneHom.instInv
- Filter.Germ.instInvOneClass
- SeparationQuotient.instInvOneClass
- Function.Injective.invOneClass