Mathlib v3 is deprecated. Go to Mathlib v4

Def linear_map.det_aux

Modification history

2023-01-16 13:27
src/linear_algebra/determinant.lean
chore(*): remove after the fact `attribute [irreducible]` at several places (#18168) …
Modified linear_map.det_auxView on Github →
2021-05-31 13:18
src/linear_algebra/determinant.lean
feat(linear_algebra): the determinant of an endomorphism (#7635) …
Added linear_map.det_auxView on Github →