Theorem eHolderNorm_eq_zero

Modification history

2024-10-12 07:45

Mathlib/Topology/MetricSpace/HolderNorm.lean

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

Added eHolderNorm_eq_zero View on Github →