isCentralScalar — Mathlib

English

If R is commutative with the scalar action, then the scalar action is central on MvPolynomial.

Русский

Если действие скаляра коммутирует, тогда действие скаляра центральное на MvPolynomial.

LaTeX

$$$ \text{IsCentralScalar}_R(\MvPolynomial(σ,S_1)) $$$

Lean4

instance isCentralScalar [CommSemiring S₁] [SMulZeroClass R S₁] [SMulZeroClass Rᵐᵒᵖ S₁] [IsCentralScalar R S₁] :
    IsCentralScalar R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.isCentralScalar

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