Theorem WithLp.prod_nndist_eq_of_L1

Modification history

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