nonsingular_neg — Mathlib

English

If W is nonsingular at P, then W.neg P is nonsingular at W.neg P, with a case split based on whether P z equals zero.

Русский

Если W не сингулярна в P, то W.neg P также не сингулярна, разбиение по случаю P z = 0 или ≠ 0.

LaTeX

$$$$W.Nonsingular P \Rightarrow W.Nonsingular (W.neg P)$$$$

Lean4

theorem nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <| W.neg P :=
  by
  by_cases hPz : P z = 0
  · simp only [neg_of_Z_eq_zero hP.left hPz, nonsingular_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg, nonsingular_zero]
  · simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz, nonsingular_neg_of_Z_ne_zero hP hPz]

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