Theorem Seminorm.ball_smul_closedBall

Modification history

2023-12-02 14:02
Mathlib/Analysis/Seminorm.lean
feat(Analysis/Seminorm): add more `*ball_smul_*ball` (#8783) …
Added Seminorm.ball_smul_closedBallView on Github →
2023-12-01 20:35
Mathlib/Analysis/Seminorm.lean
refactor: review normed group structure on `ContinuousLinearMap` (#8725) …
Deleted Seminorm.ball_smul_closedBallView on Github →
2023-11-30 10:58
Mathlib/Analysis/Seminorm.lean
feat(Analysis/Seminorm): add more `*ball_smul_*ball` (#8724) …
Added Seminorm.ball_smul_closedBallView on Github →