Theorems · Theorem · linear algebra

PiTensorProduct.add_tprodCoeff

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
  PiTensorProduct.tprodCoeff R z (Function.update f i m₁) + PiTensorProduct.tprodCoeff R z (Function.update f i m₂) =
    PiTensorProduct.tprodCoeff R z (Function.update f i (m₁ + m₂))

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleDecidableEq