no goals
ι : Type ?u.6837341
𝕜✝ : Type ?u.6837344
E : Type ?u.6837347
F : Type ?u.6837350
A : Type ?u.6837353
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedRing A
f✝ g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
𝕜 : Type u_1
f : ℝ → 𝕜
inst✝ : NormedField 𝕜
h : IntervalIntegrable f μ a b
c : 𝕜
⊢ IntervalIntegrable (fun x => f x / c) μ a b
simpa only [div_eq_mul_inv] using mul_const h c⁻¹