twoTorsionPolynomial_of_char_three

English

Over characteristic three, the discriminant of the two-torsion polynomial equals the discriminant Δ: W.twoTorsionPolynomial.disc = W.Δ.

Русский

В характеристике 3 дискриминант многочлена двойной тройной точки равен дискриминанту Δ: W.twoTorsionPolynomial.disc = W.Δ.

LaTeX

$$$ W.twoTorsionPolynomial.disc = W.\Delta $$$

Lean4

theorem twoTorsionPolynomial_of_char_three : W.twoTorsionPolynomial = ⟨1, W.b₂, -W.b₄, W.b₆⟩ :=
  by
  rw [twoTorsionPolynomial]
  ext <;> dsimp
  · linear_combination CharP.cast_eq_zero R 3
  · linear_combination W.b₄ * CharP.cast_eq_zero R 3

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