English
The map (x, y) ↦ (y, y⁻¹x) is measure-preserving from μ × ν to ν × μ.
Русский
Отображение (x, y) ↦ (y, y⁻¹x) сохраняет меру от μ × ν к ν × μ.
LaTeX
$$MeasurePreserving (fun z : G × G => (z.2, z.2⁻¹ * z.1)) (μ.prod ν) (ν.prod μ)$$
Lean4
/-- The map `(x, y) ↦ (yx, x⁻¹)` is measure-preserving.
This is the function `S⁻¹RSR` in [Halmos, §59],
where `S` is the map `(x, y) ↦ (x, xy)` and `R` is `Prod.swap`. -/
@[to_additive measurePreserving_add_prod_neg /-- The map `(x, y) ↦ (y + x, - x)` is measure-preserving. -/
]
theorem measurePreserving_mul_prod_inv [IsMulLeftInvariant ν] :
MeasurePreserving (fun z : G × G => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν) :=
by
convert (measurePreserving_prod_inv_mul_swap ν μ).comp (measurePreserving_prod_mul_swap μ ν) using 1
ext1 ⟨x, y⟩
simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]
