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.