addMap_of_Z_eq_zero_left — Mathlib

English

If Q z = 0, then addMap(P,Q) equals a negative scalar multiple of P when P z ≠ 0, reflecting the right-side Z-zero case.

Русский

Если Q z = 0, то addMap(P,Q) равна отрицательному скалярному умножению на P при P z ≠ 0 (правый случай Z=0).

LaTeX

$$W'.addMap ⟦P⟧ ⟦Q⟧ = - (Q_0 P_2) · P$$

Lean4

theorem addMap_of_Z_eq_zero_left {P : Fin 3 → F} {Q : PointClass F} (hP : W.Nonsingular P) (hQ : W.NonsingularLift Q)
    (hPz : P z = 0) : W.addMap ⟦P⟧ Q = Q := by
  revert hQ
  refine Q.inductionOn (motive := fun Q => _ → W.addMap _ Q = Q) fun Q hQ => ?_
  by_cases hQz : Q 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 hQ hQz
  ·
    rw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

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