[Merged by Bors] - feat(ContinuousMultilinearMap): add lemmas about .prod

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -610,14 +610,9 @@ variable (𝕜 E E' G G')
 def prodL :
     ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G' ≃ₗᵢ[𝕜]
       ContinuousMultilinearMap 𝕜 E (G × G') where
-  toFun f := f.1.prod f.2
-  invFun f :=
-    ((ContinuousLinearMap.fst 𝕜 G G').compContinuousMultilinearMap f,
-      (ContinuousLinearMap.snd 𝕜 G G').compContinuousMultilinearMap f)
+  __ := prodEquiv
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
-  left_inv f := by ext <;> rfl
-  right_inv f := by ext <;> rfl
   norm_map' f := opNorm_prod f.1 f.2
 
 /-- `ContinuousMultilinearMap.pi` as a `LinearIsometryEquiv`. -/

Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

@@ -299,19 +299,64 @@ theorem _root_.ContinuousLinearMap.compContinuousMultilinearMap_coe (g : M₂ 
   ext m
   rfl
 
+/-- `ContinuousMultilinearMap.prod` as an `Equiv`. -/
+@[simps apply symm_apply_fst symm_apply_snd, simps (config := .lemmasOnly) symm_apply]
+def prodEquiv :
+    (ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃) ≃
+      ContinuousMultilinearMap R M₁ (M₂ × M₃) where
+  toFun f := f.1.prod f.2
+  invFun f := ((ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f,
+    (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f)
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+theorem prod_ext_iff {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)} :
+    f = g ↔ (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
+      (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g ∧
+      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
+      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g := by
+  rw [← Prod.mk.inj_iff, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]
+
+@[ext]
+theorem prod_ext {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)}
+    (h₁ : (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
+      (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g)
+    (h₂ : (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
+      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g) : f = g :=
+  prod_ext_iff.mpr ⟨h₁, h₂⟩
+
+theorem eq_prod_iff {f : ContinuousMultilinearMap R M₁ (M₂ × M₃)}
+    {g : ContinuousMultilinearMap R M₁ M₂} {h : ContinuousMultilinearMap R M₁ M₃} :
+    f = g.prod h ↔ (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f = g ∧
+      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f = h :=
+  prod_ext_iff
+
+theorem add_prod_add [ContinuousAdd M₂] [ContinuousAdd M₃]
+    (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂) (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) :
+    (f₁ + f₂).prod (g₁ + g₂) = f₁.prod g₁ + f₂.prod g₂ :=
+  rfl
+
+theorem smul_prod_smul {S : Type*} [Monoid S] [DistribMulAction S M₂] [DistribMulAction S M₃]
+    [ContinuousConstSMul S M₂] [SMulCommClass R S M₂]
+    [ContinuousConstSMul S M₃] [SMulCommClass R S M₃]
+    (c : S) (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
+    (c • f).prod (c • g) = c • f.prod g :=
+  rfl
+
+@[simp]
+theorem zero_prod_zero :
+    (0 : ContinuousMultilinearMap R M₁ M₂).prod (0 : ContinuousMultilinearMap R M₁ M₃) = 0 :=
+  rfl
+
 /-- `ContinuousMultilinearMap.pi` as an `Equiv`. -/
 @[simps]
 def piEquiv {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
     [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)] :
     (∀ i, ContinuousMultilinearMap R M₁ (M' i)) ≃ ContinuousMultilinearMap R M₁ (∀ i, M' i) where
   toFun := ContinuousMultilinearMap.pi
   invFun f i := (ContinuousLinearMap.proj i : _ →L[R] M' i).compContinuousMultilinearMap f
-  left_inv f := by
-    ext
-    rfl
-  right_inv f := by
-    ext
-    rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
 
 /-- An equivalence of the index set defines an equivalence between the spaces of continuous
 multilinear maps. This is the forward map of this equivalence. -/
@@ -453,6 +498,16 @@ instance : AddCommGroup (ContinuousMultilinearMap R M₁ M₂) :=
   toMultilinearMap_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
     (fun _ _ => rfl) fun _ _ => rfl
 
+theorem neg_prod_neg [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃] [TopologicalAddGroup M₃]
+    (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
+    (-f).prod (-g) = - f.prod g :=
+  rfl
+
+theorem sub_prod_sub [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃] [TopologicalAddGroup M₃]
+    (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂) (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) :
+    (f₁ - f₂).prod (g₁ - g₂) = f₁.prod g₁ - f₂.prod g₂ :=
+  rfl
+
 end TopologicalAddGroup
 
 end Ring