Structures · Algebra
MonoidWithZero
A type M₀ is a “monoid with zero” if it is a monoid with zero element, and 0 is left
and right absorbing.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Shape
- One type argument · adds zero_mul, mul_zero
Extends3
Extended by3
Concrete types that are instances26
- Nat
- Real
- SeparationQuotient
- ContinuousLinearMap
- Filter.Germ
- DirectLimit
- OreLocalization
- Ordinal
- RingQuot
- FreeAlgebra
- Complex.UnitClosedDisc
- NonUnitalStarAlgHom
- NonUnitalStarRingHom
- NonUnitalRingHom
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- WithTop
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by489
- nonZeroDivisors
- zero_pow
- pow_pos
- pow_ne_zero
- MonoidWithZeroHom.valueGroup
- MonoidWithZeroHom.ValueGroup₀
- Ring.inverse
- pow_nonneg
- normalize
- pow_le_pow_left₀
- mul_div_cancel_right₀
- Units.ne_zero
- MonoidWithZeroHom.ValueGroup₀.embedding
- Irreducible.ne_zero
- ArithmeticFunction.IsMultiplicative
- mem_nonZeroDivisors_iff_ne_zero
- IsUnit.ne_zero
- mem_nonZeroDivisors_of_ne_zero
- MonoidWithZeroHom.ValueGroup₀.restrict₀
- sq_eq_sq₀
- pow_le_pow_right₀
- associated_of_dvd_dvd
- nonZeroDivisorsRight
- Ring.inverse_non_unit
- nonZeroDivisorsLeft
- ne_zero_of_dvd_ne_zero
- one_le_pow₀
- Ring.inverse_unit
- mul_dvd_mul_iff_left
- nonZeroDivisors.ne_zero
- IsTopologicallyNilpotent
- not_isUnit_zero
- Module.subsingleton
- pow_right_mono₀
- Squarefree.ne_zero
- one_lt_pow₀
- pow_le_one₀
- nonZeroDivisors.coe_ne_zero
- Module.nontrivial
- pow_eq_zero_iff
- normalize_zero
- dvd_antisymm_of_normalize_eq
- Associates.out
- MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
- pow_le_pow_of_le_one
- MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
- MonoidWithZeroHom.ValueGroup₀.embedding_strictMono
- IsNilpotent.map
- sq_eq_zero_iff
- Ring.inverse_invertible