Theorems · Theorem · number theory
Nat.coprime_primes
∀ {p q : ℕ}, Nat.Prime p → Nat.Prime q → (p.Coprime q ↔ p ≠ q)- Defined in
- Mathlib.Data.Nat.Prime.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.Primestatement and proof · cited by 2,059
- Nat.Prime.two_leproof · cited by 53
- Nat.Prime.coprime_iff_not_dvdproof · cited by 38
- Nat.dvd_prime_two_leproof · cited by 3
Cited by9
Results whose statement or proof uses this declaration.
- ZMod.prime_ne_zeroproof · cited by 4
- Nat.coprime_pow_primesproof · cited by 2
- Rat.AbsoluteValue.equiv_padic_of_boundedproof · cited by 1
- Nat.minSqFacProp_divproof · cited by 1
- Nat.pairwise_coprime_pow_primeFactors_factorizationproof · cited by 1
- ArithmeticFunction.IsMultiplicative.map_prod_of_primeproof · cited by 1
- Nat.Prime.dvd_mul_of_dvd_neproof · cited by 0
- IsPGroup.disjoint_of_neproof · cited by 0
- squarefree_primorialproof · cited by 0