Commit 2025-06-11 00:55 832b4eab
View on Github →chore(Analysis/Normed/Operator/BoundedLinearMaps): centralise one variable declaration (#25677)
Noticed while reviewing #25562. Prefer {X : Type*}
over {X}
as the latter introduces a universe metavariable.
These are the only occurrences of X
in that file; #25562 will add two more.