isMulLeftInvariant_map_mul_right — Mathlib

English

The image of a left-invariant measure under left multiplication is left-invariant.

Русский

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

LaTeX

$$$\text{IsMulLeftInvariant}(μ) \Rightarrow \text{IsMulLeftInvariant}(map (g \cdot) μ)$ for any g.$$

Lean4

/-- The image of a left invariant measure under right multiplication is left invariant. -/
@[to_additive isMulLeftInvariant_map_add_right /--
    The image of a left invariant measure under right addition is left invariant. -/
    ]
instance isMulLeftInvariant_map_mul_right [IsMulLeftInvariant μ] (g : G) : IsMulLeftInvariant (map (· * g) μ) :=
  isMulLeftInvariant_map_smul (MulOpposite.op g)

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