instIsMinimalMinimal

Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.instIsMinimalMinimal

English

For any Weierstrass curve W over K, the curve W.minimal R is minimal over R.

Русский

Для любой кривой Вейерштрасса W над K кривая W.minimal над R является минимальной моделью.

LaTeX

$$$\\mathrm{IsMinimal}_R\\big(W_{\\min}\\big),$ where $W_{\\min} = W.minimal(R).$$$

Lean4

instance {W : WeierstrassCurve K} : IsMinimal R (W.minimal R) :=
  (W.exists_isMinimal R).choose_spec

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru