Commit 2023-12-02 14:02 5f9aeff5

feat(Analysis/Seminorm): add more *ball_smul_*ball (#8783) We had ball_smul_ball and closedBall_smul_closedBall. Add versions with mixed ball and closedBall. Also move this lemmas below and golf the proofs. This was already merged in #8724 but accidentally got reverted in #8725 See Zulip