nonsingular_of_Z_ne_zero — Mathlib

English

If the Z-coordinate is nonzero, then W.Nonsingular P is equivalent to the affine nonsingularity at (X/Z, Y/Z).

Русский

Если координата Z ненулевая, то несингулярность W при P эквивалентна аффинной несингулярности в точке (X/Z, Y/Z).

LaTeX

$$$P: \\mathrm{Fin}(3)\\to F,\\; P_z \\neq 0 \\Rightarrow W.Nonsingular P \\iff W.toAffine.Nonsingular (P_x/P_z, P_y/P_z)$$$

Lean4

theorem nonsingular_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.Nonsingular P ↔ W.toAffine.Nonsingular (P x / P z) (P y / P z) :=
  (nonsingular_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| nonsingular_some ..

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