gcdA'_coe

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.gcdA'_coe

English

A' equals W plus X: gcdA'(a,b) = gcdW(a,b) + gcdX(a,b) (as natural numbers).

Русский

A' равен W плюс X: gcdA'(a,b) = gcdW(a,b) + gcdX(a,b) (как натуральные числа).

LaTeX

$$$(gcdA'\, a\, b) = (gcdW\, a\, b) + (gcdX\, a\, b)$$$

Lean4

theorem gcdA'_coe : (gcdA' a b : ℕ) = gcdW a b + gcdX a b :=
  by
  dsimp [gcdA', gcdX, gcdW, XgcdType.w]
  rw [add_right_comm]

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

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

Разделы

Аффилиация

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