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