dvd_gcd

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.dvd_gcd

English

If k divides both m and n, then k divides gcd(m, n).

Русский

Если k делит и m, и n, то k делит НОД(m, n).

LaTeX

$$$ (k \\mid m) \\\\land (k \\mid n) \\\\Rightarrow k \\mid \\gcd(m,n) $$$

Lean4

theorem dvd_gcd {m n k : ℕ+} (hm : k ∣ m) (hn : k ∣ n) : k ∣ gcd m n :=
  dvd_iff.2 (Nat.dvd_gcd (dvd_iff.1 hm) (dvd_iff.1 hn))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru