addZ_ne_zero_of_X_ne

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

English

For P,Q ∈ Fin 3 → F, if P x * Q z^2 ≠ Q x * P z^2, then addZ P Q ≠ 0.

Русский

Для P,Q ∈ Fin(3)→F, если P_x Q_z^2 ≠ Q_x P_z^2, то addZ P Q не равно нулю.

LaTeX

$$$P_x Q_z^2 \\neq Q_x P_z^2 \\Rightarrow addZ(P,Q) \\neq 0$$$

Lean4

theorem addZ_ne_zero_of_X_ne {P Q : Fin 3 → R} (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) : addZ P Q ≠ 0 :=
  sub_ne_zero.mpr hx

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

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

Разделы

Аффилиация

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