Commit 2025-03-14 02:32 b6dd4542
View on Github →chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on WithLp
(#22706)
This generalizes Module
to weaker classes of action.
As the assumptions now vary by lemma, a variable
line has been inlined into the following lemmas.