mathlib

f6c030fe - feat(linear_algebra/matrix/nonsingular_inverse): inverse of a diagonal matrix is diagonal (#13827)

feat(linear_algebra/matrix/nonsingular_inverse): inverse of a diagonal matrix is diagonal (#13827) The main results are `is_unit (diagonal v) ↔ is_unit v` and `(diagonal v)⁻¹ = diagonal (ring.inverse v)`. This also generalizes `invertible.map` to `monoid_hom_class`.