Commit 2022-02-28 08:31 58c20c19

feat(measure_theory/group): add measures invariant under inversion/negation (#11954)

• Define measures invariant under inv or neg
• Prove lemmas about measures invariant under inv similar to the lemmas about measures invariant under mul
• Also provide more pi instances in arithmetic.
• Rename some integral_zero... lemmas to integral_eq_zero...
• Reformulate pi.is_mul_left_invariant_volume using nondependent functions, so that type class inference can find it for ι → ℝ)
• Add some more integration lemmas, also for multiplication