instMulAction — Mathlib

English

There is a natural MulAction of G on the set of embeddings α ↪ β given by (g • f)(a) = g • f(a).

Русский

Существует естественное действие G на множестве вложений α ↪ β, задаваемое как (g • f)(a) = g • f(a).

LaTeX

$$$ g \cdot f = (\lambda a.\ g \cdot f(a)) $$$

Lean4

@[to_additive]
instance [Group G] [MulAction G β] : MulAction G (α ↪ β) :=
  DFunLike.coe_injective.mulAction _ coe_smul

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