Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_equiv.det_symm_mul_det

Modification history

2022-03-19 11:33
src/linear_algebra/determinant.lean
feat(linear_algebra/determinant): no need for `is_domain` (#12805) …
Modified linear_equiv.det_symm_mul_detView on Github →
2021-12-06 21:05
src/linear_algebra/determinant.lean
feat(linear_algebra/determinant): linear_equiv.det_mul_det_symm (#10635) …
Added linear_equiv.det_symm_mul_detView on Github →