Theorem MeasureTheory.Lp.dist_eq_eLpNorm_neg_add

Modification history

2026-02-24 15:42
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
refactor: change definition of distance in normed group (#35037) …
Added MeasureTheory.Lp.dist_eq_eLpNorm_neg_addView on Github →