English
If a square matrix M over a domain has nonzero determinant, then M is nondegenerate.
Русский
Если детерминант квадратной матрицы M над доменом не равен нулю, то M не вырождается.
LaTeX
$$$M.det \neq 0 \Rightarrow M\ \text{Nondegenerate}$$$
Lean4
/-- If `M` has a nonzero determinant, then `M` as a bilinear form on `n → A` is nondegenerate.
See also `BilinForm.nondegenerateOfDetNeZero'` and `BilinForm.nondegenerateOfDetNeZero`.
-/
theorem nondegenerate_of_det_ne_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) : Nondegenerate M :=
by
refine nondegenerate_def.mpr fun v hv ↦ ?_
ext i
specialize hv (M.cramer (Pi.single i 1))
refine (mul_eq_zero.mp ?_).resolve_right hM
convert hv
simp only [mulVec_cramer M (Pi.single i 1), dotProduct, Pi.smul_apply, smul_eq_mul]
rw [Finset.sum_eq_single i, Pi.single_eq_same, mul_one]
· intro j _ hj
simp [hj]
· intros
have := Finset.mem_univ i
contradiction
