gcd_comm

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.gcd_comm

English

For positive integers m,n, gcd(m,n)=gcd(n,m).

Русский

Для положительных чисел m и n выполнено gcd(m,n)=gcd(n,m).

LaTeX

$$$ \gcd(m,n)=\gcd(n,m) $$$

Lean4

theorem gcd_comm {m n : ℕ+} : m.gcd n = n.gcd m := by
  apply eq
  simp only [gcd_coe]
  apply Nat.gcd_comm

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

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

Разделы

Аффилиация

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