feat(LinearAlgebra/Matrix): regularized inverse limit and trace continuity#39735

allenhaozhu wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

allenhaozhu:ltfp-matrix-regularized-inv-limitallenhaozhu/mathlib4:ltfp-matrix-regularized-inv-limitCopy head branch name to clipboard