lcm_coe — Mathlib

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

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