reduce_v — Mathlib

English

For every u in XgcdType, the v-coordinate is unchanged by reduction: (u.reduce).v = u.v.

Русский

Для всякого u из XgcdType координата v сохраняется при редукции: (u.reduce).v = u.v.

LaTeX

$$$\forall u : XgcdType, (u.reduce).v = u.v$$$

Lean4

theorem reduce_v : ∀ u : XgcdType, u.reduce.v = u.v
  | u =>
    dite (u.r = 0) (fun h => by rw [reduce_a h, finish_v u h]) fun h =>
      by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]

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