map_div_right_eq_self — Mathlib

English

If μ is left invariant, then applying right multiplication preserves left invariance.

Русский

Если μ — левая инвариантность, применение правого умножения сохраняет левую инвариантность.

LaTeX

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

Lean4

@[to_additive]
theorem map_div_right_eq_self (μ : Measure G) [IsMulRightInvariant μ] (g : G) : map (· / g) μ = μ := by
  simp_rw [div_eq_mul_inv, map_mul_right_eq_self μ g⁻¹]

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