[Merged by Bors] - feat(measure_theory/group/measure): Mapping an Haar measure under a linear iso #17771
Conversation
YaelDillies
added
awaiting-review
| instance (e : G ≃ₗ[𝕜] H) : is_add_haar_measure (μ.map e) := | ||
| e.to_add_equiv.is_add_haar_measure_map _ (e : G →ₗ[𝕜] H).continuous_of_finite_dimensional | ||
| (e.symm : H →ₗ[𝕜] G).continuous_of_finite_dimensional |
There was a problem hiding this comment.
Is finite-dimensionality only used explicitly? If so, could you also add a version where e : G ≃L[𝕜] H without finite-dimensionality assumptions?
bors d+
There was a problem hiding this comment.
Can you also use this to golf the proof of map_linear_map_add_haar_eq_smul_add_haar? (where an instance would become unnecessary, as well as a few facts like Ce or Cesymm only used to prove the instance).
There was a problem hiding this comment.
I will golf map_linear_map_add_haar_eq_smul_add_haar separately because I have more API incoming that will shorten it.
bors merge
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
…inear iso (#17771) Put together a few results into one that TC inference can use.
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
YaelDillies
changed the title
YaelDillies
removed
the
awaiting-review
Put together a few results into one that TC inference can use.