Theorem PiLp.dist_eq_of_L1

Modification history

2025-01-05 01:44
Mathlib/Analysis/Normed/Lp/PiLp.lean
feat: shorthand lemmas for the L1 norm (#20383) …
Added PiLp.dist_eq_of_L1View on Github →