mathlib

f4214def - feat(measure_theory/group, measure_theory/bochner_integration): left translate of an integral (#6936)

feat(measure_theory/group, measure_theory/bochner_integration): left translate of an integral (#6936) Translating a function on a topological group by left- (right-) multiplication by a constant does not change its integral with respect to a left- (right-) invariant measure. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>