case h
α : Type u_1
E : Type ?u.11618
F : Type u_2
𝕜 : Type ?u.11624
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
x✝ : Set α
⊢ weightedSMul 0 x✝ = OfNat.ofNat 0 x✝
α : Type u_1
E : Type ?u.11618
F : Type u_2
𝕜 : Type ?u.11624
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
⊢ weightedSMul 0 = 0
ext1
no goals
case h
α : Type u_1
E : Type ?u.11618
F : Type u_2
𝕜 : Type ?u.11624
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
x✝ : Set α
⊢ weightedSMul 0 x✝ = OfNat.ofNat 0 x✝
simp [weightedSMul]