Commit 2021-02-21 06:06 f470cc62
View on Github →feat(measure_theory/interval_integral): add simp attribute to integral_const (#6334)
By adding a simp attribute to interval_integral.integral_const, the likes of the following become possible:
import measure_theory.interval_integral
example : ∫ x:ℝ in 5..19, (12:ℝ) = 168 := by norm_num