coe_gcd

Mathlib.Algebra.GCDMonoid.Nat

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

English

The natural cast of gcd agrees with the gcd in the gcd monoid: ↑(Int.gcd i j) = GCDMonoid.gcd i j.

Русский

Приведение кNat(nod) согласуется с НОД в моноиде: ↑(Int.gcd i j) = GCDMonoid.gcd i j.

LaTeX

$$$\uparrow(\gcd(i,j)) = \gcd(i,j)$$$

Lean4

theorem coe_gcd (i j : ℤ) : ↑(Int.gcd i j) = GCDMonoid.gcd i j :=
  rfl

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

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

Разделы

Аффилиация

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