smul — Mathlib

English

For group G acting on β, there is an action of G on embeddings α ↪ β by (g • f) = f ∘ (MulAction.toPerm g).

Русский

Пусть группа G действует на β; на отображениях α ↪ β действует G через композицию с перестановкой, соответствующей g: (g • f) = f ∘ (MulAction.toPerm g).

LaTeX

$$$\text{smul on embeddings}: (g \cdot f)(a) = g \cdot f(a)$$$

Lean4

@[to_additive]
instance smul [Group G] [MulAction G β] : SMul G (α ↪ β) :=
  ⟨fun g f => f.trans (MulAction.toPerm g).toEmbedding⟩

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