Commit 2022-05-06 12:51 f6c030fe
View on Github →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.