Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-08 10:55
2bbfacf9
View on Github →
feat(Holder): basic lemmas for
HolderWith
(
#16411
)
Estimated changes
Modified
Mathlib/Topology/MetricSpace/Holder.lean
added
theorem
HolderWith.add
added
theorem
HolderWith.const
added
theorem
HolderWith.mono
added
theorem
HolderWith.of_isEmpty
added
theorem
HolderWith.smul
added
theorem
HolderWith.zero
added
theorem
holderWith_zero_iff