mulLeft — Mathlib

English

Left multiplication by g defines a measurable automorphism of G.

Русский

Левое умножение на g задаёт измеримый автоморфизм G.

LaTeX

$$$$ \\text{mulLeft}(g) : G \\to G \\text{ is a measurable equivalence; } x \\mapsto g x. $$$$

Lean4

/-- If `G` is a group with measurable multiplication, then left multiplication by `g : G` is a
measurable automorphism of `G`. -/
@[to_additive /-- If `G` is an additive group with measurable addition, then addition of `g : G`
          on the left is a measurable automorphism of `G`. -/
    ]
def mulLeft (g : G) : G ≃ᵐ G :=
  smul g

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