Theorem Seminorm.closedBall_smul_ball

Modification history

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