no goals
α : Type u_2
E : Type ?u.940098
F : Type ?u.940101
𝕜 : Type ?u.940104
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
simpa only [← div_eq_mul_inv] using integral_mul_right r⁻¹ f