xgcdAux_val

Mathlib.Algebra.EuclideanDomain.Basic

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

English

The value of xgcdAux at (x,1,0,y,0,1) is the pair (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 : R) : 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