English
The map (x, y) ↦ (y, yx) sends μ × ν to ν × μ; i.e., swapping factors after left-multiplication preserves product measure.
Русский
Отображение (x, y) ↦ (y, yx) переводит μ × ν в ν × μ; сохранение мер после перестановки факторов.
LaTeX
$$MeasurePreserving (fun z : G × G => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (ν.prod μ)$$
Lean4
/-- The map `(x, y) ↦ (y, yx)` sends the measure `μ × ν` to `ν × μ`.
This is the map `SR` in [Halmos, §59].
`S` is the map `(x, y) ↦ (x, xy)` and `R` is `Prod.swap`. -/
@[to_additive measurePreserving_prod_add_swap /-- The map `(x, y) ↦ (y, y + x)` sends the measure `μ × ν` to `ν × μ`. -/
]
theorem measurePreserving_prod_mul_swap [IsMulLeftInvariant μ] :
MeasurePreserving (fun z : G × G => (z.2, z.2 * z.1)) (μ.prod ν) (ν.prod μ) :=
(measurePreserving_prod_mul ν μ).comp measurePreserving_swap
