nonsingularLift_zero

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

English

The lift of the zero orbit yields a nonsingular point when the base is nontrivial.

Русский

Лифт орбиты нуля даёт несингулярную точку, если основание непустое.

LaTeX

$$$W'.NonsingularLift \\langle 0,1,0\\rangle$ is nonsingular in lift when R is nontrivial$$

Lean4

theorem nonsingularLift_zero [Nontrivial R] : W'.NonsingularLift ⟦![0, 1, 0]⟧ :=
  nonsingular_zero

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

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

Разделы

Аффилиация

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