Commit 2021-05-16 18:58 aedd12da

refactor(measure_theory/haar_measure): move general material to content.lean, make content a structure (#7615) Several facts that are proved only for the Haar measure (including for instance regularity) are true for any measure constructed from a content. We move these facts to the content.lean file (and make content a structure for easier management). Also, move the notion of regular measure to its own file, and make it a class.