negMap_of_Z_ne_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] in the corresponding quotient.

Русский

При P ∈ Fin 3 → F с W.Nonsingular P и P_z ≠ 0 отображение отрицания даёт вектор \\[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_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.negMap ⟦P⟧ = ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧ := by
  rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]

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