mathlib

48c4f400 - refactor(measure_theory): make `volume` a bundled measure (#3075)

refactor(measure_theory): make `volume` a bundled measure (#3075) This way we can `apply` and `rw` lemmas about `measure`s without introducing a `volume`-specific version.