smul — Mathlib

English

If h is a fundamental domain for G, then for any g ∈ G, the translated set g • s is also a fundamental domain (with the same μ).

Русский

Если h — фундаментальная область для G, то для любого g ∈ G множество g • s тоже фундаментальная область (для той же μ).

LaTeX

$$$\\text{IsFundamentalDomain}(G, g\\cdot s, μ)$$$

Lean4

@[to_additive]
theorem smul (h : IsFundamentalDomain G s μ) (g : G) : IsFundamentalDomain G (g • s) μ :=
  h.image_of_equiv (MulAction.toPerm g) (measurePreserving_smul _ _).quasiMeasurePreserving
    ⟨fun g' => g⁻¹ * g' * g, fun g' => g * g' * g⁻¹, fun g' => by simp [mul_assoc], fun g' => by simp [mul_assoc]⟩
    fun g' x => by simp [smul_smul, mul_assoc]

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