addZ_ne_zero_of_X_ne

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

← MathLib Explorer

English

If P_x Q_z ≠ Q_x P_z, then addZ(P,Q) ≠ 0.

Русский

Если P_x Q_z ≠ Q_x P_z, то addZ(P,Q) ≠ 0.

LaTeX

$$If $P_x Q_z \neq Q_x P_z$, then $W'.addZ(P,Q) \neq 0$.$$

Lean4

theorem addZ_ne_zero_of_X_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ≠ Q x * P z) : W'.addZ P Q ≠ 0 :=
  addZ_eq' hP hQ ▸ left_ne_zero_of_mul <| pow_ne_zero 3 <| sub_ne_zero.mpr hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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