English
There is a natural CompatibleSMul structure on units, making Sˣ act compatibly on tensor products.
Русский
Существует естественная структура совместимой умножения на единицах, делающая действие на тензорном произведении согласованным.
LaTeX
$$$$\\text{CompatibleSMul}\\; R\\; S^\\!\\!\\!\\!\\! \\; M \\; N$$$$
Lean4
/-- While the tensor product will automatically inherit a ℤ-module structure from
`AddCommGroup.toIntModule`, that structure won't be compatible with lemmas like `tmul_smul` unless
we use a `ℤ-Module` instance provided by `TensorProduct.left_module`.
When `R` is a `Ring` we get the required `TensorProduct.compatible_smul` instance through
`IsScalarTower`, but when it is only a `Semiring` we need to build it from scratch.
The instance diamond in `compatible_smul` doesn't matter because it's in `Prop`.
-/
instance int : CompatibleSMul R ℤ M P :=
⟨fun r m p =>
Int.induction_on r (by simp) (fun r ih => by simpa [add_smul, tmul_add, add_tmul] using ih) fun r ih => by
simpa [sub_smul, tmul_sub, sub_tmul] using ih⟩
