mulRight — Mathlib

English

Right multiplication by g defines a measurable equivalence on G.

Русский

Правая установка на g задаёт измеримое эквивалентное отображение на G.

LaTeX

$$$$ \\mathrm{mulRight}(g) : G \\simeq^\\mathrm{m} G \\text{ defined by } x \\mapsto x g. $$$$

Lean4

/-- If `G` is a group with measurable multiplication, then right 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 right is a measurable automorphism of `G`. -/
    ]
def mulRight (g : G) : G ≃ᵐ G where
  toEquiv := Equiv.mulRight g
  measurable_toFun := measurable_mul_const g
  measurable_invFun := measurable_mul_const g⁻¹

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