Theorems · Definition · number theory
IsRelPrime
{α : Type u_1} → [Monoid α] → α → α → Propx and y are relatively prime if every common divisor is a unit.
- Defined in
- Mathlib.Algebra.Divisibility.Units
- Cited by
- 136 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 19 definitions · uses no axioms
- 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.
Cited by136
Results whose statement or proof uses this declaration.
- IsRelPrime.symmstatement and proof · cited by 12
- isRelPrime_commstatement · cited by 8
- IsFractionRing.num_den_reducedstatement · cited by 6
- IsRelPrime.add_mul_left_leftstatement and proof · cited by 5
- IsRelPrime.isCoprimestatement and proof · cited by 5
- IsRelPrime.of_add_mul_left_leftstatement and proof · cited by 5
- Irreducible.isRelPrime_iff_not_dvdstatement and proof · cited by 4
- IsRelPrime.dvd_of_dvd_mul_rightstatement and proof · cited by 4
- IsRelPrime.neg_left_iffstatement and proof · cited by 4
- IsRelPrime.of_mul_left_leftstatement and proof · cited by 4
- IsRelPrime.prod_rightstatement · cited by 4
- squarefree_mul_iffstatement and proof · cited by 4