xgcdAux_val

Mathlib.Data.Int.GCD

URI: https://scilib.ai/kg/mathlib#Nat.xgcdAux_val

English

The pair xgcdAux(x,1,0,y,0,1) equals (gcd(x,y), xgcd(x,y)).

Русский

Пара xgcdAux(x,1,0,y,0,1) равна (gcd(x,y), xgcd(x,y)).

LaTeX

$$$xgcdAux(x,1,0,y,0,1) = (\gcd(x,y), xgcd(x,y))$$$

Lean4

theorem xgcdAux_val (x y) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y) := by rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]

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

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

Разделы

Аффилиация

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