Det of family is non-zero iff linearly independent

Stream: Is there code for X?

[Xavier Roblot]

I think the following result has been already discussed but I don't see it in Mathlib:

import Mathlib.LinearAlgebra.Determinant
import Mathlib.LinearAlgebra.FiniteDimensional

theorem Matrix.det_ne_zero_iff {K : Type*} [Field K] {ι : Type*} [DecidableEq ι] [Fintype ι]
    {v : ι → (ι → K)} :
    (Matrix.of fun i ↦ v i).det ≠ 0 ↔ LinearIndependent K v := by
  by_cases hι : Nonempty ι
  · rw [← isUnit_iff_ne_zero, ← Pi.basisFun_det_apply, ← is_basis_iff_det, and_iff_left_iff_imp]
    exact fun h ↦ h.span_eq_top_of_card_eq_finrank (Module.finrank_fintype_fun_eq_card K).symm
  · rw [not_nonempty_iff] at hι
    simp

[Eric Wieser]

I think the version that was discussed previously was the more general version in terms of an alternating map