feat(linear_algebra/determinant): specialize is_basis.iff_det (#7668)

After the bundled basis refactor, applying `is_basis.iff_det` in the forward direction is slightly more involved (since defining the `iff` requires an unbundled basis), so I added a lemma that does the necessary translation between "unbundled basis" and "bundled basis" for you.

Author: Vierkantor

src/linear_algebra/determinant.lean

@@ -105,7 +105,7 @@ lemma basis.det_apply (v : ι → M) : e.det v = det (e.to_matrix v) := rfl
 lemma basis.det_self : e.det e = 1 :=
 by simp [e.det_apply]
 
-lemma is_basis.iff_det {v : ι → M} :
+lemma is_basis_iff_det {v : ι → M} :
   linear_independent R v ∧ span R (set.range v) = ⊤ ↔ is_unit (e.det v) :=
 begin
   split,
@@ -123,3 +123,6 @@ begin
     rw ← this,
     exact ⟨v'.linear_independent, v'.span_eq⟩ },
 end
+
+lemma basis.is_unit_det (e' : basis ι R M) : is_unit (e.det e') :=
+(is_basis_iff_det e).mp ⟨e'.linear_independent, e'.span_eq⟩