Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_equiv.map_det

Modification history

2021-10-22 15:58

src/linear_algebra/matrix/determinant.lean

feat(linear_algebra/matrix/determinant): det_conj_transpose (#9879) …

Added ring_equiv.map_det View on Github →