Structures · Algebra
MulZeroOneClass
A typeclass for non-associative monoids with zero elements.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Shape
- One type argument · adds zero_mul, mul_zero
Extends2
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances17
- Nat
- SeparationQuotient
- Filter.Germ
- LocallyConstant
- EReal
- DirectLimit
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- Shrink
- WithTop
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by234
- MonoidWithZeroHom.ofClass
- MonoidWithZeroHom.toMonoidHom
- MonoidWithZeroHom.toZeroHom
- MonoidWithZeroHom.comp
- map_ne_zero
- OrderMonoidWithZeroHom.comp
- mul_boole
- WithZero.lift'
- MonoidWithZeroHom.map_ite_one_zero
- map_eq_zero
- Invertible.ne_zero
- MulEquiv.toMonoidWithZeroHom
- Matrix.IsAdjMatrix.toGraph
- MonoidWithZeroHom.mk.congr_simp
- Finsupp.smul_single_one
- MonoidWithZeroHom.one_apply_of_ne_zero
- MonoidWithZeroHom.coe_mk
- right_ne_zero_of_mul_eq_one
- MonoidWithZeroHom.one_apply_zero
- mul_eq_right₀
- subsingleton_iff_zero_eq_one
- MonoidWithZeroHom.id
- left_ne_zero_of_mul_eq_one
- LocallyConstant.charFn
- MonoidWithZeroHom.map_one
- SignType.castHom
- eq_zero_of_mul_eq_self_left
- OrderMonoidWithZeroHom.id
- OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom
- SimpleGraph.adjMatrix_hadamard_diagonal
- SimpleGraph.diagonal_hadamard_adjMatrix
- mul_eq_left₀
- MonoidWithZeroHom.map_mul
- Set.indicator_eq_one_iff_mem
- OrderMonoidWithZeroHom.toMonoidWithZeroHom
- MonoidWithZeroHom.map_zero
- Submonoid.pos
- MonoidWithZeroHom.comp_apply
- right_eq_mul₀
- Set.inter_indicator_one
- DualNumber.inr_eq_smul_eps
- boole_mul
- MonoidWithZeroHom.map_one'
- Matrix.IsAdjMatrix.toGraph_adj
- MonoidWithZeroHom.ENatMap
- Matrix.IsAdjMatrix.toGraphReindexIso
- MonoidWithZeroHom.withTopMap
- HahnSeries.order_one
- SimpleGraph.incMatrix_apply_mul_incMatrix_apply
- MonoidWithZeroHom.map_mul'