toAffine_of_singular

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

If a projective point is singular, its affine image is identically zero.

Русский

Если точка проектной кривой сингулярна, её афинное изображение равно нулю.

LaTeX

$$$ toAffine W P = 0 \quad \text{if } W.Nonsingular P \text{ is false}$$$

Lean4

theorem toAffine_of_singular {P : Fin 3 → F} (hP : ¬W.Nonsingular P) : toAffine W P = 0 := by
  rw [toAffine, dif_neg <| not_and_of_not_left _ hP]

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

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

Разделы

Аффилиация

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