Commit 2020-08-29 17:36 4c4243c5
View on Github →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.