coe_smul — Mathlib

English

Let G be a group acting on β and α an arbitrary type, with f: α ↪ β an embedding. The action of G on embeddings is defined pointwise by (g • f)(a) = g • f(a). Hence the underlying function of g • f coincides with applying g to the image of f.

Русский

Пусть G — группа действует на β, α — произвольное множество, и f: α ↪ β — вложение. Действие G на отображения задаётся поэлементно: (g • f)(a) = g • f(a). Следовательно, прообраз функции g • f совпадает с действием g на образе f.

LaTeX

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

Lean4

@[to_additive]
theorem coe_smul [Group G] [MulAction G β] (g : G) (f : α ↪ β) : ⇑(g • f) = g • ⇑f :=
  rfl

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