English
If R' acts on M and N with a structure compatible with R via an IsScalarTower, then there is a natural CompatibleSMul instance giving a functorial action of R' on M ⊗_R N compatible with the actions on M and N.
Русский
Если R' действует на M и N в соответствии с R через IsScalarTower, то существует естественный экземпляр CompatibleSMul, задающий каноническое действие R' на M ⊗_R N, совместимое с действиями на M и N.
LaTeX
$$$\\exists\\,\\text{CompatibleSMul }(R,R',M,N)$$$
Lean4
/-- Note that this provides the default `CompatibleSMul R R M N` instance through
`IsScalarTower.left`. -/
instance (priority := 100) isScalarTower [SMul R' R] [IsScalarTower R' R M] [DistribMulAction R' N]
[IsScalarTower R' R N] : CompatibleSMul R R' M N :=
⟨fun r m n => by
conv_lhs => rw [← one_smul R m]
conv_rhs => rw [← one_smul R n]
rw [← smul_assoc, ← smul_assoc]
exact Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_smul _ _ _⟩
