mathlib3
fabc5101 - feat(linear_algebra/determinant): `linear_equiv.det_conj` (#11340)

Commit

4 years ago

feat(linear_algebra/determinant): `linear_equiv.det_conj` (#11340) Add a version of the `linear_map.det_conj` lemma for `linear_equiv.det`.

Author

jsm28

Parents