toShortNFOfCharThree_spec — Mathlib

English

If the b₂ coefficient vanishes in characteristic 3, then the short NF obtained by the CharThree change is indeed a short NF.

Русский

Если коэффициент b₂ равен нулю в характеристике 3, то краткая нормальная форма, полученная через преобразование CharThree, действительно является ShortNF.

LaTeX

$$$(hb_2 : W.b_2 = 0) \Rightarrow (W.toShortNFOfCharThree \cdot W).IsShortNF$$$

Lean4

theorem toShortNFOfCharThree_spec (hb₂ : W.b₂ = 0) : (W.toShortNFOfCharThree • W).IsShortNF :=
  by
  have h : (2 : R) * 2 = 1 := by linear_combination CharP.cast_eq_zero R 3
  letI : Invertible (2 : R) := ⟨2, h, h⟩
  have H := W.toCharNeTwoNF_spec
  exact ⟨H.a₁, hb₂ ▸ W.toShortNFOfCharThree_a₂, H.a₃⟩

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