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.

Estimated changes