instIsCentralScalar — Mathlib

English

If S is a central scalar in k, then S acts centrally on SkewMonoidAlgebra k G, i.e., s • f = f • s for all s ∈ S and f ∈ SkewMonoidAlgebra k G.

Русский

Если S — центральный скаляр в k, то S действует центрально на SkewMonoidAlgebra k G: s • f = f • s для всех s ∈ S, f ∈ SkewMonoidAlgebra k G.

LaTeX

$$$ \text{IsCentralScalar } S (SkewMonoidAlgebra k G) $$$

Lean4

instance [AddMonoid k] [SMulZeroClass S k] [SMulZeroClass Sᵐᵒᵖ k] [IsCentralScalar S k] :
    IsCentralScalar S (SkewMonoidAlgebra k G) :=
  ⟨fun _ ⟨_⟩ ↦ by simp_rw [← ofFinsupp_smul, op_smul_eq_smul]⟩

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