no goals
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ c • ball 0 1 = ball 0 ‖c‖
rw [_root_.smul_ball hc, smul_zero, mul_one]