Commit 2023-11-30 10:58 9e9a528e
View on Github →feat(Analysis/Seminorm): add more *ball_smul_*ball (#8724)
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.