Commit 2021-12-06 21:05 a8c086fe
View on Github →feat(linear_algebra/determinant): linear_equiv.det_mul_det_symm (#10635)
Add lemmas that the determinants of a linear_equiv and its
inverse multiply to 1. There are a few other lemmas involving
determinants and linear_equiv, but apparently not this one.