φ_four — Mathlib

English

The fourth φ equals the combination φ_4 = X(preΨ_4)^2 ψ_2^2 − (preΨ_4) ψ_2^4 Ψ_3 + Ψ_3^4.

Русский

φ_4 = X(preΨ_4)^2 ψ_2^2 − (preΨ_4) ψ_2^4 Ψ_3 + Ψ_3^4.

LaTeX

$$$\\phi_4 = X(\\text{pre}\\Psi_4)^2 \\psi_2^2 - (\\text{pre}\\Psi_4) \\psi_2^4 \\Psi_3 + \\Psi_3^4$$$

Lean4

@[simp]
theorem φ_four : W.φ 4 = C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4 :=
  by
  rw [φ, ψ_four, show (4 + 1 : ℤ) = 2 * 2 + 1 by rfl, ψ_odd, two_add_two_eq_four, ψ_four, show (2 - 1 : ℤ) = 1 by rfl,
    ψ_two, ψ_one, two_add_one_eq_three, show (4 - 1 : ℤ) = 3 by rfl, ψ_three]
  ring1

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