Φ_two — Mathlib

English

For index 2, Φ_2 equals a polynomial expression in X and the invariants b4, b6, b8 of the Weierstrass curve.

Русский

Для индекса 2 Φ_2 выражается как полином в X и инвариантах b4, b6, b8 кривой Вейерштрасса.

LaTeX

$$$W.\\Φ 2 = (X^4) - (C W.b₄) X^2 - (C (2 W.b₆)) X - C W.b₈$$$

Lean4

@[simp]
theorem Φ_two : W.Φ 2 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈ :=
  by
  rw [show 2 = ((1 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_two, if_neg Nat.not_even_one, Ψ₂Sq, preΨ'_three, preΨ'_one,
    if_neg Nat.not_even_one, Ψ₃]
  C_simp
  ring1

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