Structures · Algebra
MulOne
Bundling a Mul and One structure together without any axioms about their
compatibility. See MulOneClass for the additional assumption that 1 is an identity.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances2
- Matrix
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by83
- MonoidHom.comp
- MonoidHom.id
- MonoidHomClass.toMonoidHom
- MonoidHom.toOneHom
- MonoidHom.map_mul
- MonoidHom.id_apply
- MonoidHom.map_one
- MonoidHom.mk.congr_simp
- Monoid.End
- MonoidHom.comp_apply
- MonoidHom.toMulHom
- MonoidHom.coe_coe
- map_mul_eq_one
- MonoidHomClass.toMonoidHom.congr_simp
- FunLike.coeMonoidHom
- MonoidHom.map_mul'
- mul_eq_one_comm
- MonoidHom.comp_assoc
- MonoidHom.coe_comp
- Matrix.mul_eq_one_comm_of_equiv
- IsDedekindFiniteMonoid.of_injective
- MonoidHom.one_apply
- MonoidHom.cancel_right
- MonoidHom.comp_one
- isDedekindFiniteMonoid_iff
- MonoidHom.copy
- MonoidHom.id_comp
- Monoid.End.equiv
- MonoidHom.toOneHom_coe
- FunLike.coe_coeMonoidHom
- FunLike.coeMonoidHom_injective
- MonoidHom.coe_mk
- MonoidHom.comp_id
- MulEquivClass.isDedekindFiniteMonoid_iff
- FunLike.coeMonoidHom_apply
- instIsStablyFiniteRingMulOpposite
- Monoid.End.instMonoidHomClass
- FunLike.coe_coeMonoidHom'
- Monoid.End.instMonoid
- Monoid.End.instFunLike
- MonoidHom.cancel_left
- MonoidHom.toFun_eq_coe
- MonoidHom.mk_coe
- Matrix.instIsStablyFiniteRing
- MonoidHom.map_exists_left_inv
- instInhabitedMonoidHom
- Matrix.instIsDedekindFiniteMonoidOfIsStablyFiniteRing
- MulOpposite.isStablyFiniteRing_iff
- instCoeTCMonoidHomOfMonoidHomClass
- Monoid.End.instOne