no goals
ι : Type ?u.13479101
𝕜✝ : Type ?u.13479104
E : Type ?u.13479107
F : Type ?u.13479110
A : Type ?u.13479113
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ (∫ (x : ℝ) in a..b, f x / r ∂μ) = (∫ (x : ℝ) in a..b, f x ∂μ) / r
simpa only [div_eq_mul_inv] using integral_mul_const r⁻¹ f