English
For positive integers n and m, the least common multiple of n and m, when viewed as a natural number, equals Nat.lcm(n, m).
Русский
Пусть n и m — положительные числа; НОК(n, m), приведённый к обычному натуральному числу, равен Nat.lcm(n, m).
LaTeX
$$$ (\\\\lcm n m : \\\\mathbb{N}) = \\\\operatorname{Nat.lcm}(n, m) $$$
Lean4
@[simp, norm_cast]
theorem lcm_coe (n m : ℕ+) : (lcm n m : ℕ) = Nat.lcm n m :=
rfl