isMulRightInvariant_map_mul_left — Mathlib

English

The image of a left-invariant measure under left multiplication is right-invariant when viewed from the right action perspective.

Русский

Образ слева инвариантной меры при левом умножении является правой инвариантной мерой в соответствующей правой перспективе действий.

LaTeX

$$$\text{IsMulRightInvariant}(map (g \cdot) μ)$ from left action of μ.$$

Lean4

/-- The image of a right invariant measure under left multiplication is right invariant. -/
@[to_additive isMulRightInvariant_map_add_left /--
    The image of a right invariant measure under left addition is right invariant. -/
    ]
instance isMulRightInvariant_map_mul_left [IsMulRightInvariant μ] (g : G) : IsMulRightInvariant (map (g * ·) μ) :=
  isMulRightInvariant_map_smul g

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