instSMulCommClassTensorAlgebra — Mathlib

English

If R, S are commutative semirings and A, M carry appropriate module structures, then the tensor algebra T_A M carries a SMulCommClass structure, i.e., R and S actions commute on TensorAlgebra A M.

Русский

При наличии соответствующих структур модулей тензорная алгебра T_A M поддерживает структуру SMulCommClass, то есть действия R и S взаимно коммутируют на TensorAlgebra A M.

LaTeX

$$SMulCommClass R S (TensorAlgebra A M)$$

Lean4

instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A] [Algebra R A] [Algebra S A]
    [Module R M] [Module S M] [Module A M] [IsScalarTower R A M] [IsScalarTower S A M] :
    SMulCommClass R S (TensorAlgebra A M) :=
  RingQuot.instSMulCommClass _

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