Commit 2021-05-24 11:01 0b51a72c

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.