English
Again, the tensor lifting preserves semiconjugacy in the tmul setting.
Русский
Снова сохранение полусопряжённости при переходе в tmul-образование.
LaTeX
$$$ \text{SemiconjBy } a_1 a_2 a_3 \rightarrow \text{SemiconjBy } b_1 b_2 b_3 \rightarrow \text{SemiconjBy } (a_1 \otimes_R b_1) (a_2 \otimes_R b_2) (a_3 \otimes_R b_3) $$$
Lean4
instance (priority := 100) sMulCommClass_right [Monoid S] [DistribMulAction S A] [SMulCommClass S A A]
[SMulCommClass R S A] : SMulCommClass S (A ⊗[R] B) (A ⊗[R] B) where
smul_comm r x
y := by
change r • (x * y) = x * r • 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, mul_smul_comm]
| add x y hx hy => simp [smul_add, add_mul _, *]
| add x y hx hy => simp [smul_add, mul_add _, *]
