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 _