toAffine_of_Z_eq_zero

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

If the Z-coordinate of P is zero, the affine image is zero.

Русский

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

LaTeX

$$$P_z = 0 \\Rightarrow \\text{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