Changed notation wedge

urkud · Jan 16, 2025 · 83ae027 · 83ae027
1 parent 48f28e2
commit 83ae027
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean b/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean
@@ -25,21 +25,21 @@ def wedge_product (g : M [⋀^Fin m]→L[𝕜] N) (h : M [⋀^Fin n]→L[𝕜] N
   uncurryFinAdd (f.compContinuousAlternatingMap₂ g h)
 
 -- TODO: change notation
-notation f "∧" "[" g "," h "]" => wedge_product g h f
+notation g "∧["f"]" h => wedge_product g h f
 
 theorem wedge_product_def {g : M [⋀^Fin m]→L[𝕜] N} {h : M [⋀^Fin n]→L[𝕜] N'}
     {f : N →L[𝕜] N' →L[𝕜] N''} {x : Fin (m + n) → M}:
-    (f ∧ [g, h]) x = uncurryFinAdd (f.compContinuousAlternatingMap₂ g h) x :=
+    (g ∧[f] h) x = uncurryFinAdd (f.compContinuousAlternatingMap₂ g h) x :=
   rfl
 
 /- The wedge product wrt multiplication -/
 theorem wedge_product_mul {g : M [⋀^Fin m]→L[𝕜] 𝕜} {h : M [⋀^Fin n]→L[𝕜] 𝕜} {x : Fin (m + n) → M} :
-    (ContinuousLinearMap.mul 𝕜 𝕜 ∧ [g, h]) x = uncurryFinAdd ((ContinuousLinearMap.mul 𝕜 𝕜).compContinuousAlternatingMap₂ g h) x :=
+    (g ∧[ContinuousLinearMap.mul 𝕜 𝕜] h) x = uncurryFinAdd ((ContinuousLinearMap.mul 𝕜 𝕜).compContinuousAlternatingMap₂ g h) x :=
   rfl
 
 /- The wedge product wrt scalar multiplication -/
 theorem wedge_product_lsmul {g : M [⋀^Fin m]→L[𝕜] 𝕜} {h : M [⋀^Fin n]→L[𝕜] N} {x : Fin (m + n) → M} :
-    (ContinuousLinearMap.lsmul 𝕜 𝕜 ∧ [g, h]) x = uncurryFinAdd ((ContinuousLinearMap.lsmul 𝕜 𝕜).compContinuousAlternatingMap₂ g h) x :=
+    (g ∧[ContinuousLinearMap.lsmul 𝕜 𝕜] h) x = uncurryFinAdd ((ContinuousLinearMap.lsmul 𝕜 𝕜).compContinuousAlternatingMap₂ g h) x :=
   rfl
 
 end wedge
diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
@@ -205,20 +205,20 @@ def wedge_product (ω₁ : Ω^m⟮E, F⟯) (ω₂ : Ω^n⟮E, F'⟯) (f : F →L
     Ω^(m + n)⟮E, F''⟯ := fun e => ContinuousAlternatingMap.wedge_product (ω₁ e) (ω₂ e) f
 
 -- TODO: change notation
-notation f "∧" "[" ω₁ "," ω₂ "]" => wedge_product ω₁ ω₂ f
+notation ω₁ "∧["f"]" ω₂ => wedge_product ω₁ ω₂ f
 
 theorem wedge_product_def {ω₁ : Ω^m⟮E, F⟯} {ω₂ : Ω^n⟮E, F'⟯} {f : F →L[ℝ] F' →L[ℝ] F''}
-    {x : E} : (f ∧ [ω₁, ω₂]) x = ContinuousAlternatingMap.wedge_product (ω₁ x) (ω₂ x) f :=
+    {x : E} : (ω₁ ∧[f] ω₂) x = ContinuousAlternatingMap.wedge_product (ω₁ x) (ω₂ x) f :=
   rfl
 
 /- The wedge product wrt multiplication -/
 theorem wedge_product_mul {ω₁ : Ω^m⟮E, ℝ⟯} {ω₂ : Ω^n⟮E, ℝ⟯} {x : E} :
-    (ContinuousLinearMap.mul ℝ ℝ ∧ [ω₁, ω₂]) x =
+    (ω₁ ∧[ContinuousLinearMap.mul ℝ ℝ] ω₂) x =
     ContinuousAlternatingMap.wedge_product (ω₁ x) (ω₂ x) (ContinuousLinearMap.mul ℝ ℝ) :=
   rfl
 
 /- The wedge product wrt scalar multiplication -/
 theorem wedge_product_lsmul {ω₁ : Ω^m⟮E, ℝ⟯} {ω₂ : Ω^n⟮E, F⟯} {x : E} :
-    (ContinuousLinearMap.lsmul ℝ ℝ ∧ [ω₁, ω₂]) x =
+    (ω₁ ∧[ContinuousLinearMap.lsmul ℝ ℝ] ω₂) x =
     ContinuousAlternatingMap.wedge_product (ω₁ x) (ω₂ x) (ContinuousLinearMap.lsmul ℝ ℝ) :=
   rfl