dvd_gcd_mul_iff_dvd_mul — Mathlib

English

For any m,n,k, k divides gcd(k,m)·n if and only if k divides m·n.

Русский

Для любых m,n,k: k делит gcd(k,m)·n тогда и только тогда, когда k делит m·n.

LaTeX

$$$k \\mid (\\\\gcd(k,m) \\cdot n) \\quad \\Leftrightarrow \\quad k \\mid (m \\cdot n)$$$

Lean4

theorem dvd_gcd_mul_iff_dvd_mul [GCDMonoid α] {m n k : α} : k ∣ gcd k m * n ↔ k ∣ m * n :=
  ⟨fun h => h.trans (mul_dvd_mul (gcd_dvd_right k m) dvd_rfl), dvd_gcd_mul_of_dvd_mul⟩

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