Commit 2024-09-08 10:55 2bbfacf9

View on Github →

feat(Holder): basic lemmas for HolderWith (#16411)

Estimated changes

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