mathlib3
dc4e5cb4 - chore(analysis): move lemmas around (#12621)

Commit
3 years ago
chore(analysis): move lemmas around (#12621) * move `smul_unit_ball` to `analysis.normed_space.pointwise`, rename it to `smul_unit_ball_of_pos`; * reorder lemmas in `analysis.normed_space.pointwise`; * add `vadd_ball_zero`, `vadd_closed_ball_zero`, `smul_unit`, `affinity_unit_ball`, `affinity_unit_closed_ball`. Co-authored-by: Yaƫl Dillies <yael.dillies@gmail.com>
Author
Parents
Loading