English
The external ring action is additive: (r + s) · x = r · x + s · x for all r,s ∈ R', x ∈ M ⊗_R N.
Русский
Действие внешней кольца по сложению является аддитивным: (r + s) · x = r · x + s · x для всех r,s ∈ R', x ∈ M ⊗_R N.
LaTeX
$$$\forall r,s \in R',\; \forall x \in M \otimes_R N:\; (r+s)\cdot x = r\cdot x + s\cdot x$$$
Lean4
protected theorem add_smul (r s : R'') (x : M ⊗[R] N) : (r + s) • x = r • x + s • x :=
have : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
x.induction_on (by simp_rw [TensorProduct.smul_zero, add_zero]) (fun m n => by simp_rw [this, add_smul, add_tmul])
fun x y ihx ihy => by
simp_rw [TensorProduct.smul_add]
rw [ihx, ihy, add_add_add_comm]