chore(linear_algebra/multilinear): Add `linear_map.comp_multilinear_m…

…ap_dom_dom_congr` (#5270)
leanprover-community · Dec 9, 2020 · e357a33 · e357a33
1 parent 698d6b7
commit e357a33
Showing 1 changed file with 10 additions and 2 deletions.
diff --git a/src/linear_algebra/multilinear.lean b/src/linear_algebra/multilinear.lean
@@ -484,8 +484,9 @@ end semiring
 end multilinear_map
 
 namespace linear_map
-variables [semiring R] [Πi, add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃]
-[∀i, semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃]
+variables [semiring R]
+[Πi, add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M']
+[∀i, semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃] [semimodule R M']
 
 /-- Composing a multilinear map with a linear map gives again a multilinear map. -/
 def comp_multilinear_map (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) :
@@ -500,6 +501,13 @@ def comp_multilinear_map (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M
 lemma comp_multilinear_map_apply (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) (m : Π i, M₁ i) :
   g.comp_multilinear_map f m = g (f m) := rfl
 
+variables {ι₁ ι₂ : Type*} [decidable_eq ι₁] [decidable_eq ι₂]
+
+@[simp] lemma comp_multilinear_map_dom_dom_congr (σ : ι₁ ≃ ι₂) (g : M₂ →ₗ[R] M₃)
+  (f : multilinear_map R (λ i : ι₁, M') M₂) :
+  (g.comp_multilinear_map f).dom_dom_congr σ = g.comp_multilinear_map (f.dom_dom_congr σ) :=
+by { ext, simp }
+
 end linear_map
 
 namespace multilinear_map