nonsingular_neg — Mathlib

English

If P is nonsingular, then W.neg P is nonsingular as well.

Русский

Если P несингулярна, то и W.neg P несингулярна.

LaTeX

$$$\forall {F : Type},\ [\text{Field }F],\ \forall {W : \mathrm{Jacobian}(F)},\ \forall P : \mathrm{Fin}_3 \to F,\ 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 hPz,
      nonsingular_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_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]

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