Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 22:32 f4214def

View on Github →

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.

Estimated changes