English
For a Weierstrass curve W over a field K with a discrete valuation ring R, there exists a nonzero element u in K such that the scaled curve u · W is a minimal Weierstrass model over R.
Русский
Для кривой Вейерштрасса W над полем K с дискретной оценкой R существует ненулевой элемент u из K такой, что кривую u · W можно привести к минимальной модели Вейерштрасса над R.
LaTeX
$$$\\exists u \\in K^{\\times},\\; \\mathrm{IsMinimal}_R(u \\cdot W).$$$
Lean4
/-- A minimal Weierstrass equation for a given Weierstrass curve over `K`. -/
noncomputable def minimal (W : WeierstrassCurve K) : WeierstrassCurve K :=
(W.exists_isMinimal R).choose • W