second_contAux_eq — Mathlib

English

If the zeroth state is gp, then the second auxiliary continuation equals the pair ⟨gp.b · h + gp.a, gp.b⟩.

Русский

Если нулевое состояние равно gp, то второй вспомогательный элемент продолжения равен паре ⟨gp.b · h + gp.a, gp.b⟩.

LaTeX

$$$ g.contsAux 2 = \\langle gp.b \\cdot g.h + gp.a, gp.b \\rangle \\quad$ при $g.s.get? 0 = \\text{some } gp$$$

Lean4

theorem second_contAux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
    g.contsAux 2 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by simp [zeroth_s_eq, contsAux, nextConts, nextDen, nextNum]

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