lcm_eq_mul

Mathlib.Data.Nat.GCD.Basic

URI: https://scilib.ai/kg/mathlib#Nat.Coprime.lcm_eq_mul

English

If m and n are coprime, then lcm(m,n) = m·n.

Русский

Если m и n взаимно просты, то наименьшее общее кратное равно произведению.

LaTeX

$$$\text{Coprime}(m,n) \Rightarrow \mathrm{lcm}(m,n) = m \cdot n.$$$

Lean4

theorem lcm_eq_mul {m n : ℕ} (h : Coprime m n) : lcm m n = m * n := by
  rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]

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

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

Разделы

Аффилиация

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