α : Type u_2
E : Type ?u.936450
F : Type ?u.936453
𝕜 : Type ?u.936456
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
L : Type u_1
inst✝ : IsROrC L
r : L
f : α → L
⊢ (∫ (a : α), r * f a ∂μ) = r * ∫ (a : α), f a ∂μ
α : Type u_2
E : Type ?u.936450
F : Type ?u.936453
𝕜 : Type ?u.936456
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
L : Type u_1
inst✝ : IsROrC L
r : L
f : α → L
⊢ (∫ (a : α), f a * r ∂μ) = (∫ (a : α), f a ∂μ) * r
simp only [mul_comm]
no goals
α : Type u_2
E : Type ?u.936450
F : Type ?u.936453
𝕜 : Type ?u.936456
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
L : Type u_1
inst✝ : IsROrC L
r : L
f : α → L
⊢ (∫ (a : α), r * f a ∂μ) = r * ∫ (a : α), f a ∂μ
exact integral_mul_left r f