feat(linear_algebra): determinant of vectors in a basis (#3919)
From the sphere eversion project, define the determinant of a family of vectors with respects to a basis.
The main result is `is_basis.iff_det` asserting a family of vectors is a basis iff its determinant in some basis is invertible.
Also renames `equiv_fun_basis` to `is_basis.equiv_fun` and `equiv_fun_basis_symm_apply` to `is_basis.equiv_fun_symm_apply`, in order to use dot notation.
Co-authored-by: Anne Baanen t.baanen@vu.nl
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
