nonsingularLift_iff

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Projective.nonsingularLift_iff

English

If W′ is nonsingular at P, then the lifted object is nonsingular at its quotient, and vice versa.

Русский

Если W′ несингулярна в P, то её лифтинг по орбите несингулярен на класс; и наоборот.

LaTeX

$$$W'.NonsingularLift(\\overline{P}) \\iff W'.Nonsingular P$$$

Lean4

theorem nonsingularLift_iff (P : Fin 3 → R) : W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P :=
  Iff.rfl

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

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

Разделы

Аффилиация

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