Theorems · Theorem · linear algebra

PiTensorProduct.smul_add

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
  [inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] (r : R₁) (x y : PiTensorProduct R fun i => s i),
  r • (x + y) = r • x + r • y

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

0 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleMonoidDistribMulActionSMulCommClass