eq_one_of_dvd_coprimes — Mathlib

English

If a and b are coprime and k divides both a and b, then k = 1.

Русский

Пусть a и b взаимно просты и k делит оба числа; тогда k = 1.

LaTeX

$$$\forall a,b,k \in \mathbb{N}, \gcd(a,b)=1 \land k \mid a \land k \mid b \Rightarrow k = 1$$$

Lean4

/-- If `k:ℕ` divides coprime `a` and `b` then `k = 1` -/
theorem eq_one_of_dvd_coprimes {a b k : ℕ} (h_ab_coprime : Coprime a b) (hka : k ∣ a) (hkb : k ∣ b) : k = 1 :=
  dvd_one.mp (isUnit_iff_dvd_one.mp <| coprime_iff_isRelPrime.mp h_ab_coprime hka hkb)

Похожие утверждения