preΨ_even — Mathlib

English

For any Weierstrass curve W and integer m, the even-index relation holds: preΨ(2m) = preΨ(m−1)^2 · preΨ(m) · preΨ(m+2) − preΨ(m−2) · preΨ(m) · preΨ(m+1)^2.

Русский

Пусть W — кривая Вейерштрасса и m — целое число. Соотношение для чётного индекса: preΨ(2m) = preΨ(m−1)^2 · preΨ(m) · preΨ(m+2) − preΨ(m−2) · preΨ(m) · preΨ(m+1)^2.

LaTeX

$$$W.pre\\Psi(2m) = W.pre\\Psi(m-1)^2 \cdot W.pre\\Psi(m) \cdot W.pre\\Psi(m+2) - W.pre\\Psi(m-2) \cdot W.pre\\Psi(m) \cdot W.pre\\Psi(m+1)^2$$$

Lean4

theorem preΨ_even (m : ℤ) :
    W.preΨ (2 * m) = W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2 :=
  preNormEDS_even ..

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