Theorems · Definition · group theory
Associated
{M : Type u_1} → [Monoid M] → M → M → PropTwo elements of a Monoid are Associated if one of them is another one
multiplied by a unit on the right.
- Defined in
- Mathlib.Algebra.GroupWithZero.Associated
- Cited by
- 296 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 28 definitions · uses no axioms
- 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.
Cited by307
Results whose statement or proof uses this declaration.
- Associated.symmstatement and proof · cited by 87
- Associated.dvdstatement and proof · cited by 38
- associated_iff_eqstatement · cited by 28
- associated_of_dvd_dvdstatement and proof · cited by 28
- Associated.reflstatement · cited by 25
- UniqueFactorizationMonoid.prod_normalizedFactorsstatement and proof · cited by 23
- Associated.transstatement and proof · cited by 22
- UniqueFactorizationMonoid.factors_prodstatement and proof · cited by 18
- Associates.mk_eq_mk_iff_associatedstatement · cited by 16
- Ideal.span_singleton_eq_span_singletonstatement · cited by 15
- UniqueFactorizationMonoid.factors_uniquestatement and proof · cited by 14
- associated_one_iff_isUnitstatement and proof · cited by 14
Showing the 200 most cited of 307.