gcd_def

Mathlib.Data.Int.GCD

URI: https://scilib.ai/kg/mathlib#Int.gcd_def

English

For integers i and j, the gcd of i and j equals the gcd of their absolute values as natural numbers.

Русский

Для целых чисел i и j НОД(i, j) равен НОД(|i|, |j|) как натуральных чисел.

LaTeX

$$$$\\gcd(i,j) = \\mathrm{gcd}(\\lvert i\\rvert, \\lvert j\\rvert).$$$$

Lean4

theorem gcd_def (i j : ℤ) : gcd i j = Nat.gcd i.natAbs j.natAbs :=
  rfl

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

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

Разделы

Аффилиация

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