smulCommClass

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.smulCommClass

← MathLib Explorer

English

There is a SMulCommClass: R acts commutatively with MvPolynomial σ S2.

Русский

Существует SMulCommClass: R действует перестанно с MvPolynomial σ S2.

LaTeX

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

Lean4

instance smulCommClass [CommSemiring S₂] [SMulZeroClass R S₂] [SMulZeroClass S₁ S₂] [SMulCommClass R S₁ S₂] :
    SMulCommClass R S₁ (MvPolynomial σ S₂) :=
  AddMonoidAlgebra.smulCommClass

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru