gcd_dvd_right

Mathlib.Data.PNat.Prime

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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