Structures · Algebra
MulOneClass
Typeclass for expressing that a type M with multiplication and a one satisfies
1 * a = a and a * 1 = a for all a : M.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds one_mul, mul_one
Extends1
Extended by2
Concrete types that are instances31
- Nat
- SeparationQuotient
- Filter.Germ
- BoundedContinuousFunction
- Unitization
- WithConv
- LocallyConstant
- DomMulAct
- Units
- TrivSqZeroExt
- DirectLimit
- Interval
- SetSemiring
- Tropical
- RingCon.Quotient
- SubMulAction
- Con.Quotient
- Monoid.Coprod
- MonCat.FilteredColimits.M
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- Colex
- Multiplicative
- WithOne
How is a type an instance?
Loading the hierarchy index…
Assumed by1,270
- mul_one
- one_mul
- MonoidHom.ker
- Submonoid.map
- Submonoid.comap
- Submonoid.closure
- Submonoid.toSubsemigroup
- MulEquiv.toMonoidHom
- Monoid.Coprod
- MonoidHom.mrange
- neg_one_mul
- MonoidHom.domRestrict
- Monoid.Coprod.inl
- Monoid.Coprod.inr
- Submonoid.subset_closure
- WithZero.map'
- Submonoid.smul_def
- Submonoid.op
- mul_le_of_le_one_left
- star_one
- Submonoid.mul_mem
- MonoidHom.inr
- MonoidHom.inl
- MonoidHom.snd
- MonoidAlgebra.of
- mul_neg_one
- mul_le_of_le_one_right
- MonoidHom.fst
- Submonoid.one_mem
- Submonoid.closure_induction
- Submonoid.closure_le
- Submonoid.prod
- MonoidAlgebra.of_apply
- Submonoid.unop
- Submonoid.subtype
- Monoid.Coprod.swap
- Submonoid.center
- Submonoid.le_comap_map
- MonoidHom.mker
- Con.mk'
- MonoidHom.mem_ker
- Commute.one_right
- MonoidHom.mulSingle
- neg_eq_neg_one_mul
- OrderMonoidHom.comp
- mul_add_one
- MonoidHom.toAdditive
- le_mul_of_one_le_left
- Submonoid.opEquiv
- Submonoid.saturation