simp [IsBump]
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ IsBump (f * g)
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g) ∧ ContDiff ℝ ⊤ (f * g)