preΨ'_even — Mathlib

English

For any W and any natural m, the even-index recurrence holds: preΨ'(2(m+3)) = preΨ'(m+2)^2 · preΨ'(m+3) · preΨ'(m+5) − preΨ'(m+1) · preΨ'(m+3) · preΨ'(m+4)^2.

Русский

Для любой W и любого натурального m справедлива равенство для чётных индексов: preΨ'(2(m+3)) = preΨ'(m+2)^2 · preΨ'(m+3) · preΨ'(m+5) − preΨ'(m+1) · preΨ'(m+3) · preΨ'(m+4)^2.

LaTeX

$$$\forall m \in \mathbb{N},\ W.pre\\Psi'(2(m+3)) = W.pre\\Psi'(m+2)^2 \cdot W.pre\\Psi'(m+3) \cdot W.pre\\Psi'(m+5) - W.pre\\Psi'(m+1) \cdot W.pre\\Psi'(m+3) \cdot W.pre\\Psi'(m+4)^2$$$

Lean4

theorem preΨ'_even (m : ℕ) :
    W.preΨ' (2 * (m + 3)) =
      W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2 :=
  preNormEDS'_even ..

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