instIsIntegralOfIsMinimal

Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

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

English

An instance provides IsIntegral R W whenever W is IsMinimal with respect to R.

Русский

Экземпляр обеспечивает IsIntegral R W whenever W is IsMinimal по отношению к R.

LaTeX

$$Instance: If W is IsMinimal over R, then IsIntegral R W$$

Lean4

instance {W : WeierstrassCurve K} [IsMinimal R W] : IsIntegral R W := by simpa using IsMinimal.val_Δ_maximal.1

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

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

Разделы

Аффилиация

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