mathlib3
9c8602b0 - refactor(measure_theory): add subfolder (#8594)

Commit
4 years ago
refactor(measure_theory): add subfolder (#8594) * This PR adds the subfolders `constructions` `function` `group` `integral` and `measure` to `measure_theory` * File renamings: ``` group -> group.basic prod_group -> group.prod bochner_integration -> integral.bochner integration -> integral.lebesgue haar_measure -> measure.haar lebesgue_measure -> measure.lebesgue hausdorff_measure -> measure.hausdorff ```
Author
Parents
Loading