English
Under appropriate assumptions, the right scalar action extends to a tower on tensors: IsScalarTower S (A ⊗_R B) (A ⊗_R B).
Русский
При надлежащих предположениях правая скалярная операция задаёт башню на тензорном произведении.
LaTeX
$$$ IsScalarTower S (A \otimes_R B) (A \otimes_R B) $$$
Lean4
instance (priority := 100) isScalarTower_right [Monoid S] [DistribMulAction S A] [IsScalarTower S A A]
[SMulCommClass R S A] : IsScalarTower S (A ⊗[R] B) (A ⊗[R] B) where
smul_assoc r x
y := by
change r • x * y = r • (x * y)
induction y with
| zero => simp [smul_zero]
| tmul a b =>
induction x with
| zero => simp [smul_zero]
| tmul a' b' =>
dsimp
rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
| add x y hx hy => simp [smul_add, add_mul _, *]
| add x y hx hy =>
simp [smul_add, mul_add _, *]
-- we want `Algebra.to_smulCommClass` to take priority since it's better for unification elsewhere
