Structures · Algebra
CommMonoidWithZero
A type M is a commutative “monoid with zero” if it is a commutative 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
Extends2
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances21
- Nat
- Real
- SeparationQuotient
- NNReal
- EReal
- DirectLimit
- Localization
- OreLocalization
- Cardinal
- Associates
- ValuativeRel.ValueGroupWithZero
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Lex
- ContinuousMap
- WithTop
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by1,031
- Prime
- DirichletCharacter
- UniqueFactorizationMonoid.normalizedFactors
- mul_div_cancel_left₀
- Associates.factors
- Associates.count
- IsPrimePow
- UniqueFactorizationMonoid.radical
- UniqueFactorizationMonoid.factors
- Prime.irreducible
- Associates.FactorSet
- Finset.gcd
- Prime.ne_zero
- Finset.prod_ne_zero_iff
- Finset.prod_eq_zero
- Finset.prod_le_prod
- Finset.prod_nonneg
- Finset.lcm
- WfDvdMonoid
- DvdNotUnit
- UniqueFactorizationMonoid.primeFactors
- Prime.not_isUnit
- DirichletCharacter.conductor
- DirichletCharacter.changeLevel
- normalize_eq
- Finset.prod_pos
- UniqueFactorizationMonoid.prod_normalizedFactors
- dvd_antisymm
- UniqueFactorizationMonoid.prime_of_normalized_factor
- Multiset.gcd
- Multiset.lcm
- MulChar.equivToUnitHom
- Associates.FactorSet.prod
- UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors
- UniqueFactorizationMonoid.factors_prod
- dvd_lcm_left
- dvd_lcm_right
- Prime.dvd_or_dvd
- irreducible_iff_prime
- Associates.factors'
- UniqueFactorizationMonoid.irreducible_of_normalized_factor
- MulChar.toUnitHom
- UniqueFactorizationMonoid.factors_unique
- lcm_dvd
- UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors
- UniqueFactorizationMonoid.normalizedFactors_zero
- Prime.dvd_of_dvd_pow
- UniqueFactorizationMonoid.irreducible_of_factor
- normalize_gcd
- MulChar.one_apply_coe