Theorems · Theorem · group theory
associated_of_dvd_dvd
∀ {M : Type u_1} [inst : MonoidWithZero M] [IsLeftCancelMulZero M] {a b : M}, a ∣ b → b ∣ a → Associated a b- Defined in
- Mathlib.Algebra.GroupWithZero.Associated
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_oneproof · cited by 3,885
- mul_assocproof · cited by 1,667
- MulZeroClass.zero_mulproof · cited by 1,625
- MonoidWithZerostatement and proof · cited by 456
- Associatedstatement and proof · cited by 296
- IsLeftCancelMulZerostatement and proof · cited by 48
- mul_left_cancel₀proof · cited by 47
Cited by28
Results whose statement or proof uses this declaration.
- dvd_dvd_iff_associatedproof · cited by 5
- normalize_eq_normalizeproof · cited by 5
- gcd_mul_left'proof · cited by 4
- Int.associated_natAbsproof · cited by 4
- Associated.gcdproof · cited by 4
- IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprimeproof · cited by 3
- gcd_comm'proof · cited by 2
- RatFunc.associated_num_invproof · cited by 1
- associated_gcd_left_iffproof · cited by 1
- IsFractionRing.associated_den_num_invproof · cited by 1
- Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeffproof · cited by 1
- Finset.associated_lcm_prodproof · cited by 1