feat(Analysis/CStarAlgebra/CStarMatrix): operator-monotone rpow/log/sqrt specializations#39734

allenhaozhu wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

allenhaozhu:ltfp-add-cstarmatrix-operator-monotoneallenhaozhu/mathlib4:ltfp-add-cstarmatrix-operator-monotoneCopy head branch name to clipboard