neg_of_Z_ne_zero — Mathlib

English

If P z ≠ 0, then W.neg P equals P z times the vector with coordinates given by P x / P z, W.toAffine.negY(P x / P z, P y / P z), 1.

Русский

Если P z ≠ 0, то W.neg P = P_z · [P_x / P_z, W.toAffine.negY(P_x / P_z, P_y / P_z), 1].

LaTeX

$$$$W.neg P = P_z \cdot \bigl[ \tfrac{P_x}{P_z},\; W.toAffine.negY(\tfrac{P_x}{P_z}, \tfrac{P_y}{P_z}),\; 1 \bigr]$$$$

Lean4

theorem neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] := by
  erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz, mul_one]

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