Theorems · Theorem · linear algebra

PiTensorProduct.reindex_reindex

∀ {ι : 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' : ι₂ ≃ ι₃)
  (x : PiTensorProduct R fun i => s i),
  (PiTensorProduct.reindex R (fun i => s (e.symm i)) e') ((PiTensorProduct.reindex R s e) x) =
    (PiTensorProduct.reindex R s (e.trans e')) x

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule