negMap_of_Z_eq_zero — Mathlib

English

If P ∈ Fin 3 → F with W.Nonsingular P and P z = 0, then W.negMap ⟦P⟧ equals the vector [P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1].

Русский

Пусть P ∈ Fin 3 → F удовлетворяет условию W.Nonsingular P и P z = 0; тогда W.negMap ⟦P⟧ равно вектору \\[P_x/P_z, W.toAffine.negY(P_x/P_z, P_y/P_z), 1\\].

LaTeX

$$$ W.negMap \\llbracket P \\rrbracket = \\llbracket \\dfrac{P_x}{P_z},\\; W.toAffine.negY\\left( \\dfrac{P_x}{P_z}, \\dfrac{P_y}{P_z} \\right),\\; 1 \\rrbracket $$$

Lean4

theorem negMap_of_Z_eq_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z = 0) : W.negMap ⟦P⟧ = ⟦![0, 1, 0]⟧ := by
  rw [negMap_eq, neg_of_Z_eq_zero hP.left hPz, smul_eq _ (isUnit_Y_of_Z_eq_zero hP hPz).neg]

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