instSMulCommClass — Mathlib

English

If two additive monoids act on k with a commuting action, SkewMonoidAlgebra k G inherits a SMulCommClass between them.

Русский

Если два аддитивных моноида действуют на k взаимно коммутируемым образом, SkewMonoidAlgebra k G наследует SMulCommClass между ними.

LaTeX

$$$ SMulCommClass S_1 S_2 (SkewMonoidAlgebra k G) $$$

Lean4

instance [AddMonoid k] [SMulZeroClass S₁ k] [SMulZeroClass S₂ k] [SMulCommClass S₁ S₂ k] :
    SMulCommClass S₁ S₂ (SkewMonoidAlgebra k G) :=
  ⟨fun _ _ ⟨_⟩ ↦ by simp_rw [← ofFinsupp_smul, smul_comm _ _ _]⟩

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