toAffine_of_singular

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

If a Jacobian point is singular, the affine image is defined to be zero.

Русский

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

LaTeX

$$$\\text{toAffine}(W, P) = 0 \\quad\\text{if } W\\text{ is singular at } P$$$

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