smulCommClass_left — Mathlib

English

The scalar action distributes over the decomposition of a tensor into sums of simple tensors (compatibility with add_tmul and smul_tmul).

Русский

Действие скаляра распределяется по разложению тензора на суммы простых тензоров (совместимо с add_tmul и smul_tmul).

LaTeX

$$$\forall r\in R',\; x,y:\, x + y \in M \otimes_R N \Rightarrow r\cdot(x+y) = r\cdot x + r\cdot y$$$

Lean4

/-- `SMulCommClass R' R'₂ M` implies `SMulCommClass R' R'₂ (M ⊗[R] N)` -/
instance smulCommClass_left [SMulCommClass R' R'₂ M] : SMulCommClass R' R'₂ (M ⊗[R] N) where
  smul_comm r' r'₂
    x :=
    TensorProduct.induction_on x (by simp_rw [TensorProduct.smul_zero]) (fun m n => by simp_rw [smul_tmul', smul_comm])
      fun x y ihx ihy => by simp_rw [TensorProduct.smul_add]; rw [ihx, ihy]

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