gcd_dvd_left

Mathlib.Data.PNat.Prime

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

English

For positive integers n and m, gcd(n, m) divides n.

Русский

Для положительных чисел n и m НОД(n, m) делит n.

LaTeX

$$$ \gcd(n,m) \\mid n $$$

Lean4

theorem gcd_dvd_left (n m : ℕ+) : gcd n m ∣ n :=
  dvd_iff.2 (Nat.gcd_dvd_left (n : ℕ) (m : ℕ))

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

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

Разделы

Аффилиация

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