addMap_of_Z_eq_zero_right — Mathlib

English

If the X-inequality hx holds (P_x Q_z^2 ≠ Q_x P_z^2), then addMap(P,Q) equals addZ(P,Q) multiplied by the affine coordinates given by addX/addY and a final 1 in the z-coordinate.

Русский

Если выполняется неравенство по X, то addMap(P,Q) равна addZ(P,Q) умноженному на аффинные координаты addX/addY и завершающий 1 в z-координате.

LaTeX

$$W'.addMap ⟦P⟧ ⟦Q⟧ = addZ P Q · ⟦[W.toAffine.addX(...), W.toAffine.addY(...), 1]⟧$$

Lean4

theorem addMap_of_Z_eq_zero_right {P : PointClass F} {Q : Fin 3 → F} (hP : W.NonsingularLift P) (hQ : W.Nonsingular Q)
    (hQz : Q z = 0) : W.addMap P ⟦Q⟧ = P := by
  revert hP
  refine P.inductionOn (motive := fun P => _ → W.addMap P _ = P) fun P hP => ?_
  by_cases hPz : P z = 0
  · rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz, smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]
    exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz
  ·
    rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg]

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