add_of_X_ne — Mathlib

English

If P lies on W and Q is a nonsingular lift with Q_z = 0, then adding in the map returns Q: W.addMap ⟦P⟧ Q = Q.

Русский

Если P лежит на W, а Q — несингулярный подъём с Q_z = 0, то W.addMap ⟦P⟧ Q = Q.

LaTeX

$$$ \\text{W.addMap} \\llbracket P \\rrbracket Q = Q $$$

Lean4

theorem add_of_X_ne [DecidableEq F] {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 ≠ Q x * P z) :
    W.add P Q =
      W.addZ P Q •
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
          W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
            (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
          1] :=
  by rw [add_of_not_equiv <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]

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