instIsEllipticHSMulVariableChange

English

An admissible linear change of variables preserves the ellipticity of a Weierstrass curve: if W is elliptic, then C • W is elliptic.

Русский

Допустимое линейное изменение переменных сохраняет эллиптичность кривой: если W эллиптична, то C • W тоже эллиптическая.

LaTeX

$$$\\text{If } W \\text{ is elliptic, then } (C \\cdot W).IsElliptic.$$$

Lean4

instance : (C • W).IsElliptic := by
  rw [isElliptic_iff, variableChange_Δ]
  exact (C.u⁻¹.isUnit.pow 12).mul W.isUnit_Δ

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