Commit 2024-01-11 16:24 d191734a
View on Github →chore(Analysis/NormedSpace/OperatorNorm): remove local instance in favor of letI (#9653)
The former creates defs that are just noise, and have horrible names that the doc linter will complain about if the autogenerated name changes.