b₈_of_char_three — Mathlib

English

In characteristic three, b8 equals a1^2 a6 + a2 a6 − a1 a3 a4 + a2 a3^2 − a4^2.

Русский

В характеристике три, b8 = a1^2 a6 + a2 a6 − a1 a3 a4 + a2 a3^2 − a4^2.

LaTeX

$$$$ W.b_8 = W.a_1^2 W.a_6 + W.a_2 W.a_6 - W.a_1 W.a_3 W.a_4 + W.a_2 W.a_3^2 - W.a_4^2 $$$$

Lean4

theorem b₈_of_char_three : W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 :=
  by
  rw [b₈]
  linear_combination W.a₂ * W.a₆ * CharP.cast_eq_zero R 3

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