Theorem MemHolder.smul

Modification history

2025-04-30 06:41

Mathlib/Topology/MetricSpace/HolderNorm.lean

feat: generalize `MemHolder.smul` (#24464)

Modified MemHolder.smul View on Github →

2025-03-11 08:53

Mathlib/Topology/MetricSpace/HolderNorm.lean

chore(Topology/MetricSpace): rename BoundedSMul to IsBoundedSMul (#22797) …

Modified MemHolder.smul View on Github →

2024-10-12 07:45

Mathlib/Topology/MetricSpace/HolderNorm.lean

feat(HolderNorm): Define the Hölder norm (#16711)

Added MemHolder.smul View on Github →