Mathlib Changelog
v4
Changelog
About
Github
Theorem
MemHolder.holderWith
Modification history
2024-10-12 07:45
Mathlib/Topology/MetricSpace/HolderNorm.lean
feat(HolderNorm): Define the Hölder norm (#16711)
Added
MemHolder.holderWith
View on Github →