mathlib3

f781c47e - feat(linear_algebra/determinant): specialize `linear_equiv.is_unit_det` to automorphisms (#7667)

feat(linear_algebra/determinant): specialize `linear_equiv.is_unit_det` to automorphisms (#7667) `linear_equiv.is_unit_det` is defined for all equivs between equal-dimensional spaces, using `det (linear_map.to_matrix _ _ _)`, but I needed this result for `linear_map.det _` (which only exists between the exact same space). So I added the specialization `linear_equiv.is_unit_det'`.