reduce_a — Mathlib

English

In the Xgcd algorithm, if the current remainder r is zero, then the current reduced state equals the finished state.

Русский

В алгоритме Xgcd, если текущий остаток r равен нулю, то текущие сокращённое состояние равно завершающему состоянию.

LaTeX

$$$\\forall u:\\mathrm{XgcdType},\\ u.r = 0 \\implies u.reduce = u.finish$$$

Lean4

theorem reduce_a {u : XgcdType} (h : u.r = 0) : u.reduce = u.finish :=
  by
  rw [reduce]
  exact if_pos h

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