# Commit 2020-07-17 07:23 7d31f772

View on Github →refactor(measure_theory/*): big refactor (#3373)
Big refactor of integrals, fixes #3084
Make `integral (f : α → E) (μ : measure α)`

the main definition, and use `notation`

for other integrals
(over a set and/or w.r.t. the canonical measure `volume`

).