English
For a Weierstrass curve, there is a defined change of variables giving a CharThreeNF form; this is the toCharThreeNF construction.
Русский
Для кривой Вейерштрасса существует заданное изменение переменных, приводящее к форме CharThreeNF; это построение toCharThreeNF.
LaTeX
$$$\text{toCharThreeNF} : \mathrm{WeierstrassCurve} R \to \mathrm{VariableChange}(F)$$$
Lean4
/-- For a `WeierstrassCurve` defined over a field of characteristic = 3,
there is an explicit change of variables of it to `WeierstrassCurve.IsCharThreeNF`, that is,
`Y² = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharThreeJNeZeroNF`) or
`Y² = X³ + a₄X + a₆` (`WeierstrassCurve.IsShortNF`).
It is the composition of an explicit change of variables with
`WeierstrassCurve.toShortNFOfCharThree`. -/
def toCharThreeNF : VariableChange F :=
⟨1, (W.toShortNFOfCharThree • W).a₄ / (W.toShortNFOfCharThree • W).a₂, 0, 0⟩ * W.toShortNFOfCharThree
