no goals
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ c • closedBall 0 1 = closedBall 0 ‖c‖
rw [smul_closedBall _ _ zero_le_one, smul_zero, mul_one]