Theorem MemHolder.coe_nnHolderNorm_eq_eHolderNorm

Modification history

2024-10-12 07:45
Mathlib/Topology/MetricSpace/HolderNorm.lean
feat(HolderNorm): Define the Hölder norm (#16711)
Added MemHolder.coe_nnHolderNorm_eq_eHolderNormView on Github →