instMulAction — Mathlib

English

For any subgroup H ≤ G, there is a natural action of H on α given by h • a := (h : G) • a.

Русский

Для подгруппы H ≤ G существует естественное действие H на α, заданное h • a := (h : G) • a.

LaTeX

$$$$ \\text{There is a natural action } h \\cdot a := (h : G) \\cdot a \\text{ of } H \\text{ on } \\alpha. $$$$

Lean4

@[to_additive]
instance instMulAction (H : Subgroup G) : MulAction H α :=
  inferInstanceAs (MulAction H.toSubmonoid α)

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