nondegenerate_iff_det_ne_zero — Mathlib

English

A matrix M is nondegenerate if and only if its determinant is nonzero.

Русский

Матрица M ненулеперестановочно, если и только если её детерминант не ноль.

LaTeX

$$$\\text{Nondegenerate } M \\iff \\det M \\neq 0$$$

Lean4

theorem nondegenerate_iff_det_ne_zero {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
    Nondegenerate M ↔ M.det ≠ 0 := by
  rw [ne_eq, ← exists_vecMul_eq_zero_iff]
  push_neg
  constructor
  · intro hM v hv hMv
    obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv
    simp [dotProduct_mulVec, hMv, zero_dotProduct, ne_eq] at hwMv
  · rw [Matrix.nondegenerate_def]
    intro h v hv
    refine not_imp_not.mp (h v) (funext fun i => ?_)
    simpa only [dotProduct_mulVec, dotProduct_single, mul_one] using hv (Pi.single i 1)

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