Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-09-04 15:06
adb8e37e
View on Github →
chore(Analysis/Normed/Operator): golf entire
opNorm_subsingleton
(
#28379
)
Estimated changes
Modified
Mathlib/Analysis/Normed/Operator/Basic.lean
modified
theorem
ContinuousLinearMap.opNorm_subsingleton