no goals
E : Type ?u.12725
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → ℝ
a b : ℝ
⊢ (⨍ (x : ℝ) in Ι a b, f x) = (∫ (x : ℝ) in a..b, f x) / (b - a)
rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]