reduce_b — Mathlib

English

If r ≠ 0, then u.reduce = u.step.reduce.flip; i.e., the reduction chain follows the flip of the step's reduction.

Русский

Если r ≠ 0, то u.reduce = u.step.reduce.flip; цепочка снижения следует за flip степенного снижения.

LaTeX

$$$u.r \\neq 0 \\Rightarrow u.reduce = u.step.reduce.flip$$$

Lean4

theorem reduce_b {u : XgcdType} (h : u.r ≠ 0) : u.reduce = u.step.reduce.flip :=
  by
  rw [reduce]
  exact if_neg h

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