Theorems · Definition · group theory
Associates.mk
{M : Type u_2} → [inst : Monoid M] → M → Associates MThe canonical quotient map from a monoid M into the Associates of M
- Defined in
- Mathlib.Algebra.GroupWithZero.Associated
- Cited by
- 137 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 54 definitions · uses propext
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- Associatesstatement · cited by 210
- Associated.setoidproof · cited by 10
Cited by152
Results whose statement or proof uses this declaration.
- FractionalIdeal.countproof · cited by 25
- UniqueFactorizationMonoid.prod_normalizedFactorsproof · cited by 23
- IsDedekindDomain.HeightOneSpectrum.maxPowDividingproof · cited by 17
- Associates.mk_eq_mk_iff_associatedstatement · cited by 16
- Associates.factors'proof · cited by 15
- Associates.factors_mkstatement · cited by 12
- UniqueFactorizationMonoid.normalizedFactors_mulproof · cited by 11
- IsDedekindDomain.HeightOneSpectrum.associates_irreduciblestatement · cited by 11
- IsDedekindDomain.HeightOneSpectrum.intValuation_if_negstatement · cited by 11
- Associates.irreducible_mkstatement and proof · cited by 11
- IsDedekindDomain.HeightOneSpectrum.intValuationDefproof · cited by 9
- IsDedekindDomain.HeightOneSpectrum.intValuation_le_oneproof · cited by 9