add_of_Y_ne — Mathlib

English

If P and Q are nonsingular points on W with the Y-compatibility law not holding (i.e., P_y Q_z^3 ≠ Q_y P_z^3), then the sum W.add P Q equals the scalar-addition of addU by [1,1,0]: W.add P Q = addU P Q · [1,1,0].

Русский

Если P и Q — невырожденные точки на W и Y-условие не выполняется (P_y Q_z^3 ≠ Q_y P_z^3), то сумма P+Q равна умножению суммы addU на вектор [1,1,0].

LaTeX

$$$W.add\,P\,Q = addU\,P\,Q \cdot \begin{bmatrix}1\\1\\0\end{bmatrix}$$$

Lean4

theorem add_of_Y_ne {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3) : W.add P Q = addU P Q • ![1, 1, 0] := by
  rw [add_of_not_equiv <| not_equiv_of_Y_ne hy, addXYZ_of_X_eq hP hQ hPz hQz hx]

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