feat(LinearAlgebra/Matrix): nonsingular inverse commutes with any monoid hom of matrix rings#39733

allenhaozhu wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

allenhaozhu:ltfp-add-matrix-conj-invallenhaozhu/mathlib4:ltfp-add-matrix-conj-invCopy head branch name to clipboard