Theorems · Theorem · linear algebra

PiTensorProduct.map_comp

∀ {ι : 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} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (g : (i : ι) → t i →ₗ[R] t' i) (f : (i : ι) → s i →ₗ[R] t i),
  (PiTensorProduct.map fun i => g i ∘ₗ f i) = PiTensorProduct.map g ∘ₗ PiTensorProduct.map f

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

CommSemiringAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModule