toShortNFOfCharThree_a₂ — Mathlib

English

For the short normal form obtained from CharThree, the transformed a₂ coefficient satisfies (W.toShortNFOfCharThree • W).a₂ = W.b₂.

Русский

Для краткой нормальной формы, полученной из CharThree, преобразованный коэффициент a₂ удовлетворяет (W.toShortNFOfCharThree • W).a₂ = W.b₂.

LaTeX

$$$ (W.toShortNFOfCharThree \cdot W).a_2 = W.b_2 $$$

Lean4

theorem toShortNFOfCharThree_a₂ : (W.toShortNFOfCharThree • W).a₂ = W.b₂ :=
  by
  simp_rw [toShortNFOfCharThree, toCharNeTwoNF, variableChange_a₂, inv_one, Units.val_one, b₂]
  linear_combination (-W.a₂ - W.a₁ ^ 2) * CharP.cast_eq_zero R 3

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