English
If W.b₂ ≠ 0, then the CharThreeNF obtained by the CharThreeNF construction is IsCharThreeJNeZeroNF.
Русский
Если W.b₂ ≠ 0, то полученная преобразованием CharThreeNF кривой W обладает свойством IsCharThreeJNeZeroNF.
LaTeX
$$$\forall {F} [\text{Field }F] [\text{CharP }F\,3] (W : \mathrm{WeierstrassCurve} F),\ W.b_2 \neq 0 \Rightarrow (W.toCharThreeNF \cdot W).IsCharThreeJNeZeroNF$$$
Lean4
theorem toCharThreeNF_spec_of_b₂_ne_zero (hb₂ : W.b₂ ≠ 0) : (W.toCharThreeNF • W).IsCharThreeJNeZeroNF :=
by
have h : (2 : F) * 2 = 1 := by linear_combination CharP.cast_eq_zero F 3
letI : Invertible (2 : F) := ⟨2, h, h⟩
rw [toCharThreeNF, mul_smul]
set W' := W.toShortNFOfCharThree • W
haveI : W'.IsCharNeTwoNF := W.toCharNeTwoNF_spec
constructor
· simp [variableChange_a₁]
· simp [variableChange_a₃]
· have ha₂ : W'.a₂ ≠ 0 := W.toShortNFOfCharThree_a₂ ▸ hb₂
simp [field, variableChange_a₄, -mul_eq_zero]
linear_combination (W'.a₄ * W'.a₂ ^ 2 + W'.a₄ ^ 2) * CharP.cast_eq_zero F 3
