Theorems · Theorem · number theory
Nat.eq_one_of_dvd_coprimes
∀ {a b k : ℕ}, a.Coprime b → k ∣ a → k ∣ b → k = 1If k:ℕ divides coprime a and b then k = 1
- Defined in
- Mathlib.Data.Nat.GCD.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Quot.sound
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.
- isUnit_iff_dvd_oneproof · cited by 21
- Nat.coprime_iff_isRelPrimeproof · cited by 4
Cited by8
Results whose statement or proof uses this declaration.
- Nat.coprime_primeFactorsList_disjointproof · cited by 3
- Subgroup.disjoint_of_coprime_natCardproof · cited by 3
- IsCyclic.normalizer_le_centralizerproof · cited by 2
- AddSubgroup.disjoint_of_coprime_natCardproof · cited by 1
- IsPGroup.le_or_disjoint_of_coprimeproof · cited by 1
- Nat.disjoint_divisors_filter_isPrimePowproof · cited by 1
- IsPGroup.disjoint_of_coprimeproof · cited by 1
- NumberField.Units.rootsOfUnity_eq_oneproof · cited by 0