lcm_def — Mathlib

English

The least common multiple of two integers equals the least common multiple of their absolute values as natural numbers.

Русский

Наименьшее общее кратное двух целых чисел равняется наименьшему общему кратному их абсолютных значений как натуральных чисел.

LaTeX

$$$$\\operatorname{lcm}(i,j) = \\operatorname{lcm}(\\lvert i\\rvert, \\lvert j\\rvert).$$$$

Lean4

theorem lcm_def (i j : ℤ) : lcm i j = Nat.lcm (natAbs i) (natAbs j) :=
  rfl

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