Theorems · Definition · group theory
Associates
(M : Type u_2) → [Monoid M] → Type u_2
The quotient of a monoid by the Associated relation. Two elements x and y
are associated iff there is a unit u such that x * u = y. There is a natural
monoid structure on Associates M.
- Defined in
- Mathlib.Algebra.GroupWithZero.Associated
- Cited by
- 210 results in Mathlib
- Foundations
- Depth 13 from the axioms, rests on 52 definitions · uses propext
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- Associated.setoidproof · cited by 10
Cited by236
Results whose statement or proof uses this declaration.
- Associates.mkstatement · cited by 137
- Associates.factorsstatement and proof · cited by 97
- Associates.countstatement and proof · cited by 79
- Associates.FactorSetproof · cited by 52
- UniqueFactorizationMonoid.prod_normalizedFactorsproof · cited by 23
- Associates.FactorSet.prodstatement and proof · cited by 20
- Associates.mk_eq_mk_iff_associatedstatement · cited by 16
- Associates.factors'statement · cited by 15
- Associates.outstatement · cited by 15
- Associates.factors_mkstatement · cited by 12
- IsDedekindDomain.HeightOneSpectrum.associates_irreduciblestatement · cited by 11
- Associates.irreducible_mkstatement and proof · cited by 11
Showing the 200 most cited of 236.