chore(linear_algebra/pi_tensor_product): add reindex_reindex (#10336)

leanprover-community · Nov 15, 2021 · 9074095 · 9074095
1 parent a0f2c47
commit 9074095
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/linear_algebra/pi_tensor_product.lean b/src/linear_algebra/pi_tensor_product.lean
@@ -424,6 +424,10 @@ begin
   congr,
 end
 
+@[simp] lemma reindex_reindex (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) (x : ⨂[R] i, M) :
+  reindex R M e' (reindex R M e x) = reindex R M (e.trans e') x :=
+linear_equiv.congr_fun (reindex_trans e e' : _ = reindex R M (e.trans e')) x
+
 @[simp] lemma reindex_symm (e : ι ≃ ι₂) :
   (reindex R M e).symm = reindex R M e.symm := rfl