gcdB'_coe

Mathlib.Data.PNat.Xgcd

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

English

B' equals Y plus Z: gcdB'(a,b) = gcdY(a,b) + gcdZ(a,b) (as natural numbers).

Русский

B' равен Y плюс Z: gcdB'(a,b) = gcdY(a,b) + gcdZ(a,b) (как натуральные числа).

LaTeX

$$$(gcdB'\, a\, b) = (gcdY\, a\, b) + (gcdZ\, a\, b)$$$

Lean4

theorem gcdB'_coe : (gcdB' a b : ℕ) = gcdY a b + gcdZ a b :=
  by
  dsimp [gcdB', gcdY, gcdZ, XgcdType.z]
  rw [add_assoc]

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

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

Разделы

Аффилиация

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