rightRegular — Mathlib

English

The left regular representation of G on G → k is defined by (s) • f(t) = f(s^{-1} t).

Русский

Левое регуляторное представление группы G на пространстве функций G → k задается так: (s) • f(t) = f(s^{-1} t).

LaTeX

$$$\\text{leftRegular}(s)\\, f(t) = f(s^{-1} t)$$$

Lean4

/-- The representation on `G → k` induced by multiplication on the right in `G`. -/
def rightRegular : Representation k G (G → k)
    where
  toFun
    s :=
    { toFun f t := f (t * s)
      map_add' _ _ := rfl
      map_smul' _ _ := rfl }
  map_one' := by
    ext
    simp
  map_mul' _
    _ := by
    ext
    simp [mul_assoc]

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