Theorems · Theorem · linear algebra

PiTensorProduct.reindex_trans

∀ {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃),
  PiTensorProduct.reindex R s e ≪≫ₗ PiTensorProduct.reindex R (fun i => s (e.symm i)) e' =
    PiTensorProduct.reindex R s (e.trans e')

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule