Commit 2021-12-16 09:07 d212f3eb

feat(measure_theory/measure): new class is_finite_measure_on_compacts (#10827) We have currently four independent type classes guaranteeing that a measure of compact sets is finite: is_locally_finite_measure, is_regular_measure, is_haar_measure and is_add_haar_measure. Instead of repeting lemmas for all these classes, we introduce a new typeclass saying that a measure is finite on compact sets.