Commit 2025-05-15 14:33 724bbe72
View on Github →chore(LpSeminorm/Basic): golf a norm lemma using its enorm equivalent (#24814) Follow-up to #24640: prove norm lemmas using their enorm counterpart.
chore(LpSeminorm/Basic): golf a norm lemma using its enorm equivalent (#24814) Follow-up to #24640: prove norm lemmas using their enorm counterpart.