instIsMulRightInvariant — Mathlib

English

For a measure μ on a group G with Inv G, if μ is Inv-invariant, then μ.inv = μ.

Русский

Для меры μ на группе G, если μ инвариантна относительно инверсии, то μ.inv = μ.

LaTeX

$$$\mu\text{ IsInvInvariant} \Rightarrow \mu.inv = \mu$$$

Lean4

@[to_additive]
instance instIsMulRightInvariant [IsMulRightInvariant μ] [SFinite μ] {H : Type*} [Mul H] {mH : MeasurableSpace H}
    {ν : Measure H} [MeasurableMul H] [IsMulRightInvariant ν] [SFinite ν] : IsMulRightInvariant (μ.prod ν) :=
  by
  constructor
  rintro ⟨g, h⟩
  change map (Prod.map (· * g) (· * h)) (μ.prod ν) = μ.prod ν
  rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h), map_mul_right_eq_self μ g,
    map_mul_right_eq_self ν h]

Похожие утверждения