Commit 2025-03-20 17:15 34220922

View on Github →

chore: make the A arguments explicit in {NonUnital}ContinuousFunctionalCalculus (#23155) The fact that A is implicit is annoying because, when using concrete types for R (i.e., , , or ℝ≥0), you have to provide a type ascription to the associated predicate p : A → Prop (IsStarNormal, IsSelfAdjoint or (0 ≤ ·)). When I created IsometricContinuousFunctionalCalculus I had already become aware of this difficulty, so A is explicit in that declaration. Here we simply put the non-isometric variants on the same footing.

Estimated changes