xgcdAux_rec — Mathlib

English

If r ≠ 0, then xgcdAux r s t r' s' t' equals xgcdAux (r' mod r) (s' − (r'/r)·s) (t' − (r'/r)·t) r s t.

Русский

Если r ≠ 0, то xgcdAux r s t r' s' t' равняется xgcdAux (r' mod r) (s' − (r'/r)·s) (t' − (r'/r)·t) r s t.

LaTeX

$$$$ xgcdAux(r,s,t,r',s',t') = xgcdAux(r' \\bmod r,\\; s' - (r'/r) s,\\; t' - (r'/r) t,\\; r, s, t) \\quad\\text{при } r \\neq 0. $$$$

Lean4

theorem xgcdAux_rec {r s t r' s' t' : R} (h : r ≠ 0) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t :=
  by
  conv =>
    lhs
    rw [xgcdAux]
  exact if_neg h

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