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.

Estimated changes

modified theorem WithLp.equiv_add
modified theorem WithLp.equiv_neg
modified theorem WithLp.equiv_smul
modified theorem WithLp.equiv_sub
modified theorem WithLp.equiv_symm_add
modified theorem WithLp.equiv_symm_neg
modified theorem WithLp.equiv_symm_smul
modified theorem WithLp.equiv_symm_sub
modified theorem WithLp.equiv_symm_zero
modified theorem WithLp.equiv_zero