add_smul — Mathlib

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]

Похожие утверждения