smulCommClass_set — Mathlib

English

If α, β act on γ and commute, then the induced action on sets also commutes: SMulCommClass α β (Set γ).

Русский

Если α, β действуют на γ и переставляются, то порожденное действие на множестве γ тоже переставляется: SMulCommClass α β (Set γ).

LaTeX

$$$ SMulCommClass(\,Set γ\varnothing) $$$

Lean4

@[to_additive]
instance smulCommClass_set [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Set γ) :=
  ⟨fun _ _ ↦ Commute.set_image <| smul_comm _ _⟩

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