toAffine_of_Z_eq_zero

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

If a projective point P has z-coordinate zero, then its affine image is zero.

Русский

Если z-координата P равна нулю, то афинное изображение равно нулю.

LaTeX

$$$ (P_z = 0) \Rightarrow toAffine W P = 0 $$$

Lean4

theorem toAffine_of_Z_eq_zero {P : Fin 3 → F} (hPz : P z = 0) : toAffine W P = 0 := by
  rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]

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

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

Разделы

Аффилиация

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