gcd_mul_lcm

Mathlib.Data.PNat.Prime

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

English

For positive integers n and m, gcd(n,m) · lcm(n,m) = n · m.

Русский

Для положительных чисел n и m выполнено gcd(n,m) · lcm(n,m) = n · m.

LaTeX

$$$ \\gcd(n,m) \\cdot \\operatorname{lcm}(n,m) = n \\cdot m $$$

Lean4

theorem gcd_mul_lcm (n m : ℕ+) : gcd n m * lcm n m = n * m :=
  Subtype.eq (Nat.gcd_mul_lcm (n : ℕ) (m : ℕ))

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

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

Разделы

Аффилиация

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