minimal — Mathlib

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

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