English
For a Weierstrass curve defined in characteristic 3, there is an explicit change of variables to the short normal form; this is given by toShortNFOfCharThree.
Русский
Для кривой Вейерштрасса над кольцом характеристика 3 существует явное изменение переменных к форме ShortNF; это задаётся через toShortNFOfCharThree.
LaTeX
$$$\text{toShortNFOfCharThree} : \mathrm{WeierstrassCurve} R \to \mathrm{VariableChange}(R)$$$
Lean4
/-- For a `WeierstrassCurve` defined over a ring of characteristic = 3,
there is an explicit change of variables of it to `Y² = X³ + a₄X + a₆`
(`WeierstrassCurve.IsShortNF`) if its j = 0.
This is in fact given by `WeierstrassCurve.toCharNeTwoNF`. -/
def toShortNFOfCharThree : VariableChange R :=
have h : (2 : R) * 2 = 1 := by linear_combination CharP.cast_eq_zero R 3
letI : Invertible (2 : R) := ⟨2, h, h⟩
W.toCharNeTwoNF
