Structures · Algebra
SemigroupWithZero
A type S₀ is a "semigroup with zero” if it is a semigroup 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
Extends2
Extended by2
Concrete types that are instances19
- Nat
- SeparationQuotient
- LocallyConstant
- DirectLimit
- Finsupp
- ZeroAtInftyContinuousMap
- CompactlySupportedContinuousMap
- Complex.UnitDisc
- Prod
- OrderDual
- Set.Elem
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- WithTop
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by28
- dvd_zero
- zero_dvd_iff
- eq_zero_of_zero_dvd
- SemigroupWithZero.toZero
- instSemigroupWithZeroShrink
- SemigroupWithZero.toMulZeroClass
- Function.Injective.semigroupWithZero
- ZeroAtInftyContinuousMap.instSemigroupWithZero
- ContinuousMap.instSemigroupWithZeroOfContinuousMul
- SemigroupWithZero.toSemigroup
- SemigroupWithZero.zero_mul
- MulOpposite.instSemigroupWithZero
- SeparationQuotient.instSemigroupWithZero
- WithTop.instSemigroupWithZero
- Function.Surjective.semigroupWithZero
- LocallyConstant.instSemigroupWithZero
- DirectLimit.instSemigroupWithZeroOfMulHomClassOfZeroHomClass
- CompactlySupportedContinuousMap.instSemigroupWithZeroOfContinuousMul
- ArithmeticFunction.pmul_assoc
- AddOpposite.instSemigroupWithZero
- Prod.instSemigroupWithZero
- Finsupp.instSemigroupWithZero
- Pi.semigroupWithZero
- Equiv.semigroupWithZero
- SemigroupWithZero.mul_zero
- Lex.instSemigroupWithZero
- WithBot.instSemigroupWithZero
- OrderDual.instSemigroupWithZero