Def basis.det

Modification history

2021-05-15 14:21

src/linear_algebra/determinant.lean

refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) …

Modified basis.det View on Github →

2021-05-10 07:36

src/linear_algebra/matrix.lean

refactor(*): bundle `is_basis` (#7496) …

Added basis.det View on Github →