Structures · Algebra
MulZeroClass
Typeclass for expressing that a type M₀ with multiplication and a zero satisfies
0 * a = 0 and a * 0 = 0 for all a : M₀.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Shape
- One type argument · adds zero_mul, mul_zero
Extends2
Extended by4
Forgetful instances
Provided automatically by
Concrete types that are instances20
- Nat
- SeparationQuotient
- Filter.Germ
- LocallyConstant
- DirectLimit
- Finsupp
- ZeroAtInftyContinuousMap
- CompactlySupportedContinuousMap
- ONote
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- WithTop
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by285
- MulZeroClass.mul_zero
- MulZeroClass.zero_mul
- mul_nonneg
- mul_pos
- mul_eq_zero
- mul_ne_zero_iff
- right_ne_zero_of_mul
- left_ne_zero_of_mul
- mul_nonpos_of_nonpos_of_nonneg
- mul_nonpos_of_nonneg_of_nonpos
- mul_eq_zero_of_right
- IsRegular.of_ne_zero
- Function.support_mul
- mul_neg_of_pos_of_neg
- mul_neg_of_neg_of_pos
- mul_eq_zero_of_left
- mul_eq_mul_right_iff
- pos_of_mul_pos_left
- Unitization.inr_mul
- WithTop.mul_top
- ArithmeticFunction.pmul
- mul_lt_mul''
- mul_pos_iff_of_pos_left
- WithTop.top_mul
- Set.indicator_mul_right
- mul_eq_mul_left_iff
- IsRegular.ne_zero
- mul_self_eq_zero
- Left.mul_nonneg
- Commute.zero_left
- pos_of_mul_pos_right
- Finsupp.sum_smul_index
- zero_eq_mul
- mul_eq_zero_iff_right
- IsIdempotentElem.zero
- mul_self_le_mul_self
- WithTop.mul_ne_top
- mul_pos_iff_of_pos_right
- WithTop.mul_lt_top
- Set.indicator_mul_left
- Matrix.diagonal_hadamard
- WithTop.mul_top'
- WithTop.top_mul'
- IsLeftRegular.mul_left_eq_zero_iff
- Matrix.diagonal_kronecker
- WithTop.untop₀_mul
- Finsupp.support_mul_subset_left
- Function.support_mul_subset_left
- ne_zero_and_ne_zero_of_mul
- Pi.single_mul