measure): Mapping an Haar measure under a linear iso (#17771)

Commit

3 years ago

feat(measure_theory/group/measure): Mapping an Haar measure under a linear iso (#17771) Put together a few results into one that TC inference can use.

Author

YaelDillies

Parents

56c7bf86

mathlib3 1d4a2038 - feat(measure_theory/group/measure): Mapping an Haar measure under a linear iso (#17771)

mathlib3
1d4a2038 - feat(measure_theory/group/measure): Mapping an Haar measure under a linear iso (#17771)