English
There exists a canonical R-algebra structure on TensorAlgebra A M when R, A, M carry appropriate algebra/module structures and towers align.
Русский
Существует каноническая структура R-алгебры на TensorAlgebra A M при наличии надлежащих структур алгебр/модулей и согласованности каскадов.
LaTeX
$$TensorAlgebra A M has an R-algebra structure$$
Lean4
@[nolint unusedArguments]
instance instAlgebra {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A] [Algebra R A] [Module R M] [Module A M]
[IsScalarTower R A M] : Algebra R (TensorAlgebra A M) :=
RingQuot.instAlgebra
_
-- verify there is no diamond
-- but doesn't work at `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906
