finish_v — Mathlib

English

If r = 0, the finish's v-coordinate equals the original v: finish.v = v.

Русский

Если r = 0, то finish.v = v.

LaTeX

$$$\\text{finish.v} = v$ for $r=0$$$

Lean4

theorem finish_v (hr : u.r = 0) : u.finish.v = u.v :=
  by
  let ha : u.r + u.b * u.q = u.a := u.rq_eq
  rw [hr, zero_add] at ha
  ext
  · change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b
    have : u.wp + 1 = u.w := rfl
    rw [this, ← ha, u.qp_eq hr]
    ring
  · change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b
    rw [← ha, u.qp_eq hr]
    ring

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