Φ_four — Mathlib

English

The Φ-polynomial at index 4 equals X times preΨ₄ squared times Ψ₂Sq minus Ψ₃ times a bracketed expression involving preΨ₄ and Ψ₂Sq^2 and Ψ₃^3.

Русский

Φ_4 = X preΨ₄^2 Ψ₂Sq − Ψ₃ (preΨ₄ Ψ₂Sq^2 − Ψ₃^3).

LaTeX

$$$W.\\Φ 4 = X \cdot W.preΨ_4^2 \cdot W.\\Ψ_2Sq - W.\\Ψ_3 \cdot ( W.preΨ_4 \cdot W.\\Ψ_2Sq^2 - W.\\Ψ_3^3 )$$$

Lean4

@[simp]
theorem Φ_four : W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3) :=
  by
  rw [show 4 = ((3 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_four, if_neg <| by decide, show 3 + 2 = 2 * 2 + 1 by rfl,
    preΨ'_odd, preΨ'_four, preΨ'_two, if_pos Even.zero, preΨ'_one, preΨ'_three, if_pos Even.zero, if_neg <| by decide]
  ring1

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