mathlib
aedd12da - refactor(measure_theory/haar_measure): move general material to content.lean, make content a structure (#7615)

Commit
4 years ago
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.
Author
Parents
Loading