Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.det_comm

Modification history

2021-08-20 14:42
src/linear_algebra/determinant.lean
feat(linear_algebra/determinant): `det (M ⬝ N) = det (N ⬝ M)` if `M` is invertible (#8720) …
Added matrix.det_commView on Github →