Theorems · Theorem · linear algebra

PiTensorProduct.map_update_smul

∀ {ι : 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)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) [inst_5 : DecidableEq ι] (i : ι) (c : R)
  (u : s i →ₗ[R] t i),
  PiTensorProduct.map (Function.update f i (c • u)) = c • PiTensorProduct.map (Function.update f i u)

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleDecidableEq