Theorem Finsupp.edist_def

Modification history

2026-06-27 13:04
Mathlib/Analysis/Normed/Lp/Finsupp.lean
feat(Topology/MetricSpace): the L^p direct sum of metric spaces (#40212) …
Added Finsupp.edist_defView on Github →