instSMulCommClass — Mathlib

English

If G and G' act on β with commuting actions (SMulCommClass G G' β), then their induced actions on α ↪ β also commute: g • (h • f) = h • (g • f) for all g ∈ G, h ∈ G', f: α ↪ β.

Русский

Если действия G и G' на β коммютативны (SMulCommClass G G' β), то аналогичные действия на α ↪ β тоже коммутируют: g • (h • f) = h • (g • f).

LaTeX

$$$ g \cdot (h \cdot f) = h \cdot (g \cdot f) $$$

Lean4

@[to_additive]
instance [Group G] [Group G'] [MulAction G β] [MulAction G' β] [SMulCommClass G G' β] : SMulCommClass G G' (α ↪ β) :=
  ⟨fun x y z => Function.Embedding.ext fun i => smul_comm x y (z i)⟩

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