Right-invariant Haar measure

Stream: Is there code for X?

[Aaron Hill]

Do we have some variant of MeasureTheory.Measure.haar, but constructed to be IsMulRightInvariant instead of IsMulLeftInvariant?

[Yaël Dillies]

Can you haar on the opposite group Gᵐᵒᵖ?

[Aaron Hill]

I ended up using MeasureTheory.Measure.inv (though I had to do attribute [-simp] MeasureTheory.Measure.inv_eq_selfto unbreak simp)

[David Ledvinka]

If I understand correctly that means you are in a setting where your haar measure is inverse invariant so you should be able to prove that its also IsMulRightInvariant. I figured this is in mathlib already but I cant find it. In particular I think there should be a IsMulRightInvariant instance assuming IsMulLeftInvariant and IsInvInvariant.

[Kevin Buzzard]

If you're not inverse-invariant then another approach would be to push Haar measure along the inverse isomorphism (which is a homeomorphism).