Commit 2026-06-24 17:51 a53f9216
View on Github →feat(CStarAlgebra): IsometricCFC instance for square RCLike matrices (#40272)
Following @j-loreaux advices (see [#mathlib4 > `CFC.sqrt` continuous on positive (real) matrices](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60CFC.2Esqrt.60.20continuous.20on.20positive.20.28real.29.20matrices/with/600698185)), defines an instance of IsometricContinuousFunctionalCalculus for n × n matrices with RCLike coefficients.