Commit 2021-07-08 16:41 13486fe5

chore(measure_theory/measure_space): untangle probability_measure, finite_measure, and has_no_atoms (#8222) This only moves existing lemmas around. Putting all the instance together up front seems to result in lemmas being added in adhoc places - by adding sections, this should guide future contributions.