mathlib

a8c086fe - feat(linear_algebra/determinant): linear_equiv.det_mul_det_symm (#10635)

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.