xgcdAux_fst — Mathlib

English

In the extended gcd construction, the first component of xgcdAux x s t y s' t' equals gcd(x,y).

Русский

В конструкции расширенного НОД первый компонент xgcdAux x s t y s' t' равен gcd(x,y).

LaTeX

$$$\\operatorname{fst}(\\mathrm{xgcdAux}(x,s,t,y,s',t')) = \\gcd(x,y)$$$

Lean4

@[simp]
theorem xgcdAux_fst (x y : R) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
  GCD.induction x y
    (by
      intros
      rw [xgcd_zero_left, gcd_zero_left])
    fun x y h IH s t s' t' => by
    simp only [xgcdAux_rec h, IH]
    rw [← gcd_val]

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