diff --git a/Mathlib/Analysis/InnerProductSpace/Orientation.lean b/Mathlib/Analysis/InnerProductSpace/Orientation.lean
index 6dab7b1a12cc7..e84dd747c950c 100644
--- a/Mathlib/Analysis/InnerProductSpace/Orientation.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Orientation.lean
@@ -93,7 +93,7 @@ theorem det_eq_neg_det_of_opposite_orientation (h : e.toBasis.orientation ≠ f.
   rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
   -- Porting note: added `neg_one_smul` with explicit type
   simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h,
-    neg_one_smul ℝ (M := E [Λ^ι]→ₗ[ℝ] ℝ)]
+    neg_one_smul ℝ (M := E [⋀^ι]→ₗ[ℝ] ℝ)]
 #align orthonormal_basis.det_eq_neg_det_of_opposite_orientation OrthonormalBasis.det_eq_neg_det_of_opposite_orientation
 
 section AdjustToOrientation
@@ -178,10 +178,10 @@ variable [_i : Fact (finrank ℝ E = n)] (o : Orientation ℝ E (Fin n))
 /-- The volume form on an oriented real inner product space, a nonvanishing top-dimensional
 alternating form uniquely defined by compatibility with the orientation and inner product structure.
 -/
-irreducible_def volumeForm : E [Λ^Fin n]→ₗ[ℝ] ℝ := by
+irreducible_def volumeForm : E [⋀^Fin n]→ₗ[ℝ] ℝ := by
   classical
     cases' n with n
-    · let opos : E [Λ^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
+    · let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
       exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
     · exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
 #align orientation.volume_form Orientation.volumeForm
diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
index 65ea7dc5a3b8d..20a33366fa112 100644
--- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
+++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
@@ -93,10 +93,10 @@ namespace Orientation
 notation `ω`). When evaluated on two vectors, it gives the oriented area of the parallelogram they
 span. -/
 irreducible_def areaForm : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := by
-  let z : E [Λ^Fin 0]→ₗ[ℝ] ℝ ≃ₗ[ℝ] ℝ :=
+  let z : E [⋀^Fin 0]→ₗ[ℝ] ℝ ≃ₗ[ℝ] ℝ :=
     AlternatingMap.constLinearEquivOfIsEmpty.symm
-  let y : E [Λ^Fin 1]→ₗ[ℝ] ℝ →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
-    LinearMap.llcomp ℝ E (E [Λ^Fin 0]→ₗ[ℝ] ℝ) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
+  let y : E [⋀^Fin 1]→ₗ[ℝ] ℝ →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
+    LinearMap.llcomp ℝ E (E [⋀^Fin 0]→ₗ[ℝ] ℝ) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
   exact y ∘ₗ AlternatingMap.curryLeftLinearMap (R' := ℝ) o.volumeForm
 #align orientation.area_form Orientation.areaForm
 
diff --git a/Mathlib/LinearAlgebra/Alternating/Basic.lean b/Mathlib/LinearAlgebra/Alternating/Basic.lean
index fddaa4d953236..50084142c1c5f 100644
--- a/Mathlib/LinearAlgebra/Alternating/Basic.lean
+++ b/Mathlib/LinearAlgebra/Alternating/Basic.lean
@@ -64,15 +64,15 @@ section
 
 variable (R M N ι)
 
-/-- An alternating map is a multilinear map that vanishes when two of its arguments are equal.
--/
+/-- An alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→ₗ[R] N`,
+is a multilinear map that vanishes when two of its arguments are equal. -/
 structure AlternatingMap extends MultilinearMap R (fun _ : ι => M) N where
   /-- The map is alternating: if `v` has two equal coordinates, then `f v = 0`. -/
   map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toFun v = 0
 #align alternating_map AlternatingMap
 
 @[inherit_doc]
-notation M " [Λ^" ι "]→ₗ[" R "] " N:100 => AlternatingMap R M N ι
+notation M " [⋀^" ι "]→ₗ[" R "] " N:100 => AlternatingMap R M N ι
 
 end
 
@@ -81,11 +81,11 @@ add_decl_doc AlternatingMap.toMultilinearMap
 
 namespace AlternatingMap
 
-variable (f f' : M [Λ^ι]→ₗ[R] N)
+variable (f f' : M [⋀^ι]→ₗ[R] N)
 
-variable (g g₂ : M [Λ^ι]→ₗ[R] N')
+variable (g g₂ : M [⋀^ι]→ₗ[R] N')
 
-variable (g' : M' [Λ^ι]→ₗ[R] N')
+variable (g' : M' [⋀^ι]→ₗ[R] N')
 
 variable (v : ι → M) (v' : ι → M')
 
@@ -96,7 +96,7 @@ open Function
 
 section Coercions
 
-instance instFunLike : FunLike (M [Λ^ι]→ₗ[R] N) (ι → M) N where
+instance instFunLike : FunLike (M [⋀^ι]→ₗ[R] N) (ι → M) N where
   coe f := f.toFun
   coe_injective' := fun f g h ↦ by
     rcases f with ⟨⟨_, _, _⟩, _⟩
@@ -105,7 +105,7 @@ instance instFunLike : FunLike (M [Λ^ι]→ₗ[R] N) (ι → M) N where
 #align alternating_map.fun_like AlternatingMap.instFunLike
 
 -- shortcut instance
-instance coeFun : CoeFun (M [Λ^ι]→ₗ[R] N) fun _ => (ι → M) → N :=
+instance coeFun : CoeFun (M [⋀^ι]→ₗ[R] N) fun _ => (ι → M) → N :=
   ⟨DFunLike.coe⟩
 #align alternating_map.has_coe_to_fun AlternatingMap.coeFun
 
@@ -119,39 +119,39 @@ theorem toFun_eq_coe : f.toFun = f :=
 -- Porting note: changed statement to reflect new `mk` signature
 @[simp]
 theorem coe_mk (f : MultilinearMap R (fun _ : ι => M) N) (h) :
-    ⇑(⟨f, h⟩ : M [Λ^ι]→ₗ[R] N) = f :=
+    ⇑(⟨f, h⟩ : M [⋀^ι]→ₗ[R] N) = f :=
   rfl
 #align alternating_map.coe_mk AlternatingMap.coe_mkₓ
 
-theorem congr_fun {f g : M [Λ^ι]→ₗ[R] N} (h : f = g) (x : ι → M) : f x = g x :=
-  congr_arg (fun h : M [Λ^ι]→ₗ[R] N => h x) h
+theorem congr_fun {f g : M [⋀^ι]→ₗ[R] N} (h : f = g) (x : ι → M) : f x = g x :=
+  congr_arg (fun h : M [⋀^ι]→ₗ[R] N => h x) h
 #align alternating_map.congr_fun AlternatingMap.congr_fun
 
-theorem congr_arg (f : M [Λ^ι]→ₗ[R] N) {x y : ι → M} (h : x = y) : f x = f y :=
+theorem congr_arg (f : M [⋀^ι]→ₗ[R] N) {x y : ι → M} (h : x = y) : f x = f y :=
   _root_.congr_arg (fun x : ι → M => f x) h
 #align alternating_map.congr_arg AlternatingMap.congr_arg
 
-theorem coe_injective : Injective ((↑) : M [Λ^ι]→ₗ[R] N → (ι → M) → N) :=
+theorem coe_injective : Injective ((↑) : M [⋀^ι]→ₗ[R] N → (ι → M) → N) :=
   DFunLike.coe_injective
 #align alternating_map.coe_injective AlternatingMap.coe_injective
 
 @[norm_cast] -- @[simp] -- Porting note (#10618): simp can prove this
-theorem coe_inj {f g : M [Λ^ι]→ₗ[R] N} : (f : (ι → M) → N) = g ↔ f = g :=
+theorem coe_inj {f g : M [⋀^ι]→ₗ[R] N} : (f : (ι → M) → N) = g ↔ f = g :=
   coe_injective.eq_iff
 #align alternating_map.coe_inj AlternatingMap.coe_inj
 
 @[ext]
-theorem ext {f f' : M [Λ^ι]→ₗ[R] N} (H : ∀ x, f x = f' x) : f = f' :=
+theorem ext {f f' : M [⋀^ι]→ₗ[R] N} (H : ∀ x, f x = f' x) : f = f' :=
   DFunLike.ext _ _ H
 #align alternating_map.ext AlternatingMap.ext
 
-theorem ext_iff {f g : M [Λ^ι]→ₗ[R] N} : f = g ↔ ∀ x, f x = g x :=
+theorem ext_iff {f g : M [⋀^ι]→ₗ[R] N} : f = g ↔ ∀ x, f x = g x :=
   ⟨fun h _ => h ▸ rfl, fun h => ext h⟩
 #align alternating_map.ext_iff AlternatingMap.ext_iff
 
 attribute [coe] AlternatingMap.toMultilinearMap
 
-instance coe : Coe (M [Λ^ι]→ₗ[R] N) (MultilinearMap R (fun _ : ι => M) N) :=
+instance coe : Coe (M [⋀^ι]→ₗ[R] N) (MultilinearMap R (fun _ : ι => M) N) :=
   ⟨fun x => x.toMultilinearMap⟩
 #align alternating_map.multilinear_map.has_coe AlternatingMap.coe
 
@@ -161,7 +161,7 @@ theorem coe_multilinearMap : ⇑(f : MultilinearMap R (fun _ : ι => M) N) = f :
 #align alternating_map.coe_multilinear_map AlternatingMap.coe_multilinearMap
 
 theorem coe_multilinearMap_injective :
-    Function.Injective ((↑) : M [Λ^ι]→ₗ[R] N → MultilinearMap R (fun _ : ι => M) N) :=
+    Function.Injective ((↑) : M [⋀^ι]→ₗ[R] N → MultilinearMap R (fun _ : ι => M) N) :=
   fun _ _ h => ext <| MultilinearMap.congr_fun h
 #align alternating_map.coe_multilinear_map_injective AlternatingMap.coe_multilinearMap_injective
 
@@ -171,7 +171,7 @@ theorem coe_multilinearMap_injective :
 -- Porting note: removed `simp`
 -- @[simp]
 theorem coe_multilinearMap_mk (f : (ι → M) → N) (h₁ h₂ h₃) :
-    ((⟨⟨f, h₁, h₂⟩, h₃⟩ : M [Λ^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) =
+    ((⟨⟨f, h₁, h₂⟩, h₃⟩ : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) =
       ⟨f, @h₁, @h₂⟩ :=
   by simp
 #align alternating_map.coe_multilinear_map_mk AlternatingMap.coe_multilinearMap_mk
@@ -246,7 +246,7 @@ section SMul
 
 variable {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N]
 
-instance smul : SMul S (M [Λ^ι]→ₗ[R] N) :=
+instance smul : SMul S (M [⋀^ι]→ₗ[R] N) :=
   ⟨fun c f =>
     { c • (f : MultilinearMap R (fun _ : ι => M) N) with
       map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }⟩
@@ -262,12 +262,12 @@ theorem coe_smul (c : S) : ↑(c • f) = c • (f : MultilinearMap R (fun _ : 
   rfl
 #align alternating_map.coe_smul AlternatingMap.coe_smul
 
-theorem coeFn_smul (c : S) (f : M [Λ^ι]→ₗ[R] N) : ⇑(c • f) = c • ⇑f :=
+theorem coeFn_smul (c : S) (f : M [⋀^ι]→ₗ[R] N) : ⇑(c • f) = c • ⇑f :=
   rfl
 #align alternating_map.coe_fn_smul AlternatingMap.coeFn_smul
 
 instance isCentralScalar [DistribMulAction Sᵐᵒᵖ N] [IsCentralScalar S N] :
-    IsCentralScalar S (M [Λ^ι]→ₗ[R] N) :=
+    IsCentralScalar S (M [⋀^ι]→ₗ[R] N) :=
   ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩
 #align alternating_map.is_central_scalar AlternatingMap.isCentralScalar
 
@@ -275,7 +275,7 @@ end SMul
 
 /-- The cartesian product of two alternating maps, as an alternating map. -/
 @[simps!]
-def prod (f : M [Λ^ι]→ₗ[R] N) (g : M [Λ^ι]→ₗ[R] P) : M [Λ^ι]→ₗ[R] (N × P) :=
+def prod (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) : M [⋀^ι]→ₗ[R] (N × P) :=
   { f.toMultilinearMap.prod g.toMultilinearMap with
     map_eq_zero_of_eq' := fun _ _ _ h hne =>
       Prod.ext (f.map_eq_zero_of_eq _ h hne) (g.map_eq_zero_of_eq _ h hne) }
@@ -283,7 +283,7 @@ def prod (f : M [Λ^ι]→ₗ[R] N) (g : M [Λ^ι]→ₗ[R] P) : M [Λ^ι]→ₗ
 #align alternating_map.prod_apply AlternatingMap.prod_apply
 
 @[simp]
-theorem coe_prod (f : M [Λ^ι]→ₗ[R] N) (g : M [Λ^ι]→ₗ[R] P) :
+theorem coe_prod (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) :
     (f.prod g : MultilinearMap R (fun _ : ι => M) (N × P)) = MultilinearMap.prod f g :=
   rfl
 #align alternating_map.coe_prod AlternatingMap.coe_prod
@@ -292,7 +292,7 @@ theorem coe_prod (f : M [Λ^ι]→ₗ[R] N) (g : M [Λ^ι]→ₗ[R] P) :
 alternating map taking values in the space of functions `Π i, N i`. -/
 @[simps!]
 def pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
-    (f : ∀ i, M [Λ^ι]→ₗ[R] N i) : M [Λ^ι]→ₗ[R] (∀ i, N i) :=
+    (f : ∀ i, M [⋀^ι]→ₗ[R] N i) : M [⋀^ι]→ₗ[R] (∀ i, N i) :=
   { MultilinearMap.pi fun a => (f a).toMultilinearMap with
     map_eq_zero_of_eq' := fun _ _ _ h hne => funext fun a => (f a).map_eq_zero_of_eq _ h hne }
 #align alternating_map.pi AlternatingMap.pi
@@ -300,7 +300,7 @@ def pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Mo
 
 @[simp]
 theorem coe_pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
-    (f : ∀ i, M [Λ^ι]→ₗ[R] N i) :
+    (f : ∀ i, M [⋀^ι]→ₗ[R] N i) :
     (pi f : MultilinearMap R (fun _ : ι => M) (∀ i, N i)) = MultilinearMap.pi fun a => f a :=
   rfl
 #align alternating_map.coe_pi AlternatingMap.coe_pi
@@ -309,7 +309,7 @@ theorem coe_pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [
 sending `m` to `f m • z`. -/
 @[simps!]
 def smulRight {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂]
-    [Module R M₁] [Module R M₂] (f : M₁ [Λ^ι]→ₗ[R] R) (z : M₂) : M₁ [Λ^ι]→ₗ[R] M₂ :=
+    [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) : M₁ [⋀^ι]→ₗ[R] M₂ :=
   { f.toMultilinearMap.smulRight z with
     map_eq_zero_of_eq' := fun v i j h hne => by simp [f.map_eq_zero_of_eq v h hne] }
 #align alternating_map.smul_right AlternatingMap.smulRight
@@ -317,12 +317,12 @@ def smulRight {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [Ad
 
 @[simp]
 theorem coe_smulRight {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂]
-    [Module R M₁] [Module R M₂] (f : M₁ [Λ^ι]→ₗ[R] R) (z : M₂) :
+    [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :
     (f.smulRight z : MultilinearMap R (fun _ : ι => M₁) M₂) = MultilinearMap.smulRight f z :=
   rfl
 #align alternating_map.coe_smul_right AlternatingMap.coe_smulRight
 
-instance add : Add (M [Λ^ι]→ₗ[R] N) :=
+instance add : Add (M [⋀^ι]→ₗ[R] N) :=
   ⟨fun a b =>
     { (a + b : MultilinearMap R (fun _ : ι => M) N) with
       map_eq_zero_of_eq' := fun v i j h hij => by
@@ -339,35 +339,35 @@ theorem coe_add : (↑(f + f') : MultilinearMap R (fun _ : ι => M) N) = f + f'
   rfl
 #align alternating_map.coe_add AlternatingMap.coe_add
 
-instance zero : Zero (M [Λ^ι]→ₗ[R] N) :=
+instance zero : Zero (M [⋀^ι]→ₗ[R] N) :=
   ⟨{ (0 : MultilinearMap R (fun _ : ι => M) N) with
       map_eq_zero_of_eq' := fun v i j _ _ => by simp }⟩
 #align alternating_map.has_zero AlternatingMap.zero
 
 @[simp]
-theorem zero_apply : (0 : M [Λ^ι]→ₗ[R] N) v = 0 :=
+theorem zero_apply : (0 : M [⋀^ι]→ₗ[R] N) v = 0 :=
   rfl
 #align alternating_map.zero_apply AlternatingMap.zero_apply
 
 @[norm_cast]
-theorem coe_zero : ((0 : M [Λ^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) = 0 :=
+theorem coe_zero : ((0 : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) = 0 :=
   rfl
 #align alternating_map.coe_zero AlternatingMap.coe_zero
 
 @[simp]
 theorem mk_zero :
-    mk (0 : MultilinearMap R (fun _ : ι ↦ M) N) (0 : M [Λ^ι]→ₗ[R] N).2 = 0 :=
+    mk (0 : MultilinearMap R (fun _ : ι ↦ M) N) (0 : M [⋀^ι]→ₗ[R] N).2 = 0 :=
   rfl
 
-instance inhabited : Inhabited (M [Λ^ι]→ₗ[R] N) :=
+instance inhabited : Inhabited (M [⋀^ι]→ₗ[R] N) :=
   ⟨0⟩
 #align alternating_map.inhabited AlternatingMap.inhabited
 
-instance addCommMonoid : AddCommMonoid (M [Λ^ι]→ₗ[R] N) :=
+instance addCommMonoid : AddCommMonoid (M [⋀^ι]→ₗ[R] N) :=
   coe_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => coeFn_smul _ _
 #align alternating_map.add_comm_monoid AlternatingMap.addCommMonoid
 
-instance neg : Neg (M [Λ^ι]→ₗ[R] N') :=
+instance neg : Neg (M [⋀^ι]→ₗ[R] N') :=
   ⟨fun f =>
     { -(f : MultilinearMap R (fun _ : ι => M) N') with
       map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }⟩
@@ -379,11 +379,11 @@ theorem neg_apply (m : ι → M) : (-g) m = -g m :=
 #align alternating_map.neg_apply AlternatingMap.neg_apply
 
 @[norm_cast]
-theorem coe_neg : ((-g : M [Λ^ι]→ₗ[R] N') : MultilinearMap R (fun _ : ι => M) N') = -g :=
+theorem coe_neg : ((-g : M [⋀^ι]→ₗ[R] N') : MultilinearMap R (fun _ : ι => M) N') = -g :=
   rfl
 #align alternating_map.coe_neg AlternatingMap.coe_neg
 
-instance sub : Sub (M [Λ^ι]→ₗ[R] N') :=
+instance sub : Sub (M [⋀^ι]→ₗ[R] N') :=
   ⟨fun f g =>
     { (f - g : MultilinearMap R (fun _ : ι => M) N') with
       map_eq_zero_of_eq' := fun v i j h hij => by
@@ -400,7 +400,7 @@ theorem coe_sub : (↑(g - g₂) : MultilinearMap R (fun _ : ι => M) N') = g -
   rfl
 #align alternating_map.coe_sub AlternatingMap.coe_sub
 
-instance addCommGroup : AddCommGroup (M [Λ^ι]→ₗ[R] N') :=
+instance addCommGroup : AddCommGroup (M [⋀^ι]→ₗ[R] N') :=
   coe_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
     (fun _ _ => coeFn_smul _ _) fun _ _ => coeFn_smul _ _
 #align alternating_map.add_comm_group AlternatingMap.addCommGroup
@@ -408,7 +408,7 @@ section DistribMulAction
 
 variable {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N]
 
-instance distribMulAction : DistribMulAction S (M [Λ^ι]→ₗ[R] N) where
+instance distribMulAction : DistribMulAction S (M [⋀^ι]→ₗ[R] N) where
   one_smul _ := ext fun _ => one_smul _ _
   mul_smul _ _ _ := ext fun _ => mul_smul _ _ _
   smul_zero _ := ext fun _ => smul_zero _
@@ -423,13 +423,13 @@ variable {S : Type*} [Semiring S] [Module S N] [SMulCommClass R S N]
 
 /-- The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise
 addition and scalar multiplication. -/
-instance module : Module S (M [Λ^ι]→ₗ[R] N) where
+instance module : Module S (M [⋀^ι]→ₗ[R] N) where
   add_smul _ _ _ := ext fun _ => add_smul _ _ _
   zero_smul _ := ext fun _ => zero_smul _ _
 #align alternating_map.module AlternatingMap.module
 
 instance noZeroSMulDivisors [NoZeroSMulDivisors S N] :
-    NoZeroSMulDivisors S (M [Λ^ι]→ₗ[R] N) :=
+    NoZeroSMulDivisors S (M [⋀^ι]→ₗ[R] N) :=
   coe_injective.noZeroSMulDivisors _ rfl coeFn_smul
 #align alternating_map.no_zero_smul_divisors AlternatingMap.noZeroSMulDivisors
 
@@ -442,7 +442,7 @@ variable (R M N)
 /-- The natural equivalence between linear maps from `M` to `N`
 and `1`-multilinear alternating maps from `M` to `N`. -/
 @[simps!]
-def ofSubsingleton [Subsingleton ι] (i : ι) : (M →ₗ[R] N) ≃ (M [Λ^ι]→ₗ[R] N) where
+def ofSubsingleton [Subsingleton ι] (i : ι) : (M →ₗ[R] N) ≃ (M [⋀^ι]→ₗ[R] N) where
   toFun f := ⟨MultilinearMap.ofSubsingleton R M N i f, fun _ _ _ _ ↦ absurd (Subsingleton.elim _ _)⟩
   invFun f := (MultilinearMap.ofSubsingleton R M N i).symm f
   left_inv _ := rfl
@@ -455,7 +455,7 @@ variable (ι) {N}
 
 /-- The constant map is alternating when `ι` is empty. -/
 @[simps (config := .asFn)]
-def constOfIsEmpty [IsEmpty ι] (m : N) : M [Λ^ι]→ₗ[R] N :=
+def constOfIsEmpty [IsEmpty ι] (m : N) : M [⋀^ι]→ₗ[R] N :=
   { MultilinearMap.constOfIsEmpty R _ m with
     toFun := Function.const _ m
     map_eq_zero_of_eq' := fun _ => isEmptyElim }
@@ -466,8 +466,8 @@ end
 
 /-- Restrict the codomain of an alternating map to a submodule. -/
 @[simps]
-def codRestrict (f : M [Λ^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) :
-    M [Λ^ι]→ₗ[R] p :=
+def codRestrict (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) :
+    M [⋀^ι]→ₗ[R] p :=
   { f.toMultilinearMap.codRestrict p h with
     toFun := fun v => ⟨f v, h v⟩
     map_eq_zero_of_eq' := fun _ _ _ hv hij => Subtype.ext <| map_eq_zero_of_eq _ _ hv hij }
@@ -486,7 +486,7 @@ namespace LinearMap
 variable {N₂ : Type*} [AddCommMonoid N₂] [Module R N₂]
 
 /-- Composing an alternating map with a linear map on the left gives again an alternating map. -/
-def compAlternatingMap (g : N →ₗ[R] N₂) : (M [Λ^ι]→ₗ[R] N) →+ (M [Λ^ι]→ₗ[R] N₂) where
+def compAlternatingMap (g : N →ₗ[R] N₂) : (M [⋀^ι]→ₗ[R] N) →+ (M [⋀^ι]→ₗ[R] N₂) where
   toFun f :=
     { g.compMultilinearMap (f : MultilinearMap R (fun _ : ι => M) N) with
       map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }
@@ -499,31 +499,31 @@ def compAlternatingMap (g : N →ₗ[R] N₂) : (M [Λ^ι]→ₗ[R] N) →+ (M [
 #align linear_map.comp_alternating_map LinearMap.compAlternatingMap
 
 @[simp]
-theorem coe_compAlternatingMap (g : N →ₗ[R] N₂) (f : M [Λ^ι]→ₗ[R] N) :
+theorem coe_compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :
     ⇑(g.compAlternatingMap f) = g ∘ f :=
   rfl
 #align linear_map.coe_comp_alternating_map LinearMap.coe_compAlternatingMap
 
 @[simp]
-theorem compAlternatingMap_apply (g : N →ₗ[R] N₂) (f : M [Λ^ι]→ₗ[R] N) (m : ι → M) :
+theorem compAlternatingMap_apply (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (m : ι → M) :
     g.compAlternatingMap f m = g (f m) :=
   rfl
 #align linear_map.comp_alternating_map_apply LinearMap.compAlternatingMap_apply
 
 theorem smulRight_eq_comp {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁]
-    [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [Λ^ι]→ₗ[R] R) (z : M₂) :
+    [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :
     f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f :=
   rfl
 #align linear_map.smul_right_eq_comp LinearMap.smulRight_eq_comp
 
 @[simp]
-theorem subtype_compAlternatingMap_codRestrict (f : M [Λ^ι]→ₗ[R] N) (p : Submodule R N)
+theorem subtype_compAlternatingMap_codRestrict (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N)
     (h) : p.subtype.compAlternatingMap (f.codRestrict p h) = f :=
   AlternatingMap.ext fun _ => rfl
 #align linear_map.subtype_comp_alternating_map_cod_restrict LinearMap.subtype_compAlternatingMap_codRestrict
 
 @[simp]
-theorem compAlternatingMap_codRestrict (g : N →ₗ[R] N₂) (f : M [Λ^ι]→ₗ[R] N)
+theorem compAlternatingMap_codRestrict (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N)
     (p : Submodule R N₂) (h) :
     (g.codRestrict p h).compAlternatingMap f =
       (g.compAlternatingMap f).codRestrict p fun v => h (f v) :=
@@ -540,44 +540,44 @@ variable {M₃ : Type*} [AddCommMonoid M₃] [Module R M₃]
 
 /-- Composing an alternating map with the same linear map on each argument gives again an
 alternating map. -/
-def compLinearMap (f : M [Λ^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) : M₂ [Λ^ι]→ₗ[R] N :=
+def compLinearMap (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) : M₂ [⋀^ι]→ₗ[R] N :=
   { (f : MultilinearMap R (fun _ : ι => M) N).compLinearMap fun _ => g with
     map_eq_zero_of_eq' := fun _ _ _ h hij => f.map_eq_zero_of_eq _ (LinearMap.congr_arg h) hij }
 #align alternating_map.comp_linear_map AlternatingMap.compLinearMap
 
-theorem coe_compLinearMap (f : M [Λ^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
+theorem coe_compLinearMap (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
     ⇑(f.compLinearMap g) = f ∘ (g ∘ ·) :=
   rfl
 #align alternating_map.coe_comp_linear_map AlternatingMap.coe_compLinearMap
 
 @[simp]
-theorem compLinearMap_apply (f : M [Λ^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) (v : ι → M₂) :
+theorem compLinearMap_apply (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) (v : ι → M₂) :
     f.compLinearMap g v = f fun i => g (v i) :=
   rfl
 #align alternating_map.comp_linear_map_apply AlternatingMap.compLinearMap_apply
 
 /-- Composing an alternating map twice with the same linear map in each argument is
 the same as composing with their composition. -/
-theorem compLinearMap_assoc (f : M [Λ^ι]→ₗ[R] N) (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂) :
+theorem compLinearMap_assoc (f : M [⋀^ι]→ₗ[R] N) (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂) :
     (f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂) :=
   rfl
 #align alternating_map.comp_linear_map_assoc AlternatingMap.compLinearMap_assoc
 
 @[simp]
-theorem zero_compLinearMap (g : M₂ →ₗ[R] M) : (0 : M [Λ^ι]→ₗ[R] N).compLinearMap g = 0 := by
+theorem zero_compLinearMap (g : M₂ →ₗ[R] M) : (0 : M [⋀^ι]→ₗ[R] N).compLinearMap g = 0 := by
   ext
   simp only [compLinearMap_apply, zero_apply]
 #align alternating_map.zero_comp_linear_map AlternatingMap.zero_compLinearMap
 
 @[simp]
-theorem add_compLinearMap (f₁ f₂ : M [Λ^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
+theorem add_compLinearMap (f₁ f₂ : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
     (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g := by
   ext
   simp only [compLinearMap_apply, add_apply]
 #align alternating_map.add_comp_linear_map AlternatingMap.add_compLinearMap
 
 @[simp]
-theorem compLinearMap_zero [Nonempty ι] (f : M [Λ^ι]→ₗ[R] N) :
+theorem compLinearMap_zero [Nonempty ι] (f : M [⋀^ι]→ₗ[R] N) :
     f.compLinearMap (0 : M₂ →ₗ[R] M) = 0 := by
   ext
   -- Porting note: Was `simp_rw [.., ← Pi.zero_def, map_zero, zero_apply]`.
@@ -587,18 +587,18 @@ theorem compLinearMap_zero [Nonempty ι] (f : M [Λ^ι]→ₗ[R] N) :
 
 /-- Composing an alternating map with the identity linear map in each argument. -/
 @[simp]
-theorem compLinearMap_id (f : M [Λ^ι]→ₗ[R] N) : f.compLinearMap LinearMap.id = f :=
+theorem compLinearMap_id (f : M [⋀^ι]→ₗ[R] N) : f.compLinearMap LinearMap.id = f :=
   ext fun _ => rfl
 #align alternating_map.comp_linear_map_id AlternatingMap.compLinearMap_id
 
 /-- Composing with a surjective linear map is injective. -/
 theorem compLinearMap_injective (f : M₂ →ₗ[R] M) (hf : Function.Surjective f) :
-    Function.Injective fun g : M [Λ^ι]→ₗ[R] N => g.compLinearMap f := fun g₁ g₂ h =>
+    Function.Injective fun g : M [⋀^ι]→ₗ[R] N => g.compLinearMap f := fun g₁ g₂ h =>
   ext fun x => by simpa [Function.surjInv_eq hf] using ext_iff.mp h (Function.surjInv hf ∘ x)
 #align alternating_map.comp_linear_map_injective AlternatingMap.compLinearMap_injective
 
 theorem compLinearMap_inj (f : M₂ →ₗ[R] M) (hf : Function.Surjective f)
-    (g₁ g₂ : M [Λ^ι]→ₗ[R] N) : g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂ :=
+    (g₁ g₂ : M [⋀^ι]→ₗ[R] N) : g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂ :=
   (compLinearMap_injective _ hf).eq_iff
 #align alternating_map.comp_linear_map_inj AlternatingMap.compLinearMap_inj
 
@@ -609,7 +609,7 @@ variable (S : Type*) [Semiring S] [Module S N] [SMulCommClass R S N]
 
 /-- Construct a linear equivalence between maps from a linear equivalence between domains. -/
 @[simps apply]
-def domLCongr (e : M ≃ₗ[R] M₂) : M [Λ^ι]→ₗ[R] N ≃ₗ[S] (M₂ [Λ^ι]→ₗ[R] N) where
+def domLCongr (e : M ≃ₗ[R] M₂) : M [⋀^ι]→ₗ[R] N ≃ₗ[S] (M₂ [⋀^ι]→ₗ[R] N) where
   toFun f := f.compLinearMap e.symm
   invFun g := g.compLinearMap e
   map_add' _ _ := rfl
@@ -639,14 +639,14 @@ end DomLcongr
 /-- Composing an alternating map with the same linear equiv on each argument gives the zero map
 if and only if the alternating map is the zero map. -/
 @[simp]
-theorem compLinearEquiv_eq_zero_iff (f : M [Λ^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M) :
+theorem compLinearEquiv_eq_zero_iff (f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M) :
     f.compLinearMap (g : M₂ →ₗ[R] M) = 0 ↔ f = 0 :=
   (domLCongr R N ι ℕ g.symm).map_eq_zero_iff
 #align alternating_map.comp_linear_equiv_eq_zero_iff AlternatingMap.compLinearEquiv_eq_zero_iff
 
-variable (f f' : M [Λ^ι]→ₗ[R] N)
-variable (g g₂ : M [Λ^ι]→ₗ[R] N')
-variable (g' : M' [Λ^ι]→ₗ[R] N')
+variable (f f' : M [⋀^ι]→ₗ[R] N)
+variable (g g₂ : M [⋀^ι]→ₗ[R] N')
+variable (g' : M' [⋀^ι]→ₗ[R] N')
 variable (v : ι → M) (v' : ι → M')
 
 open Function
@@ -726,7 +726,7 @@ section DomDomCongr
 
 This is the alternating version of `MultilinearMap.domDomCongr`. -/
 @[simps]
-def domDomCongr (σ : ι ≃ ι') (f : M [Λ^ι]→ₗ[R] N) : M [Λ^ι']→ₗ[R] N :=
+def domDomCongr (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι']→ₗ[R] N :=
   { f.toMultilinearMap.domDomCongr σ with
     toFun := fun v => f (v ∘ σ)
     map_eq_zero_of_eq' := fun v i j hv hij =>
@@ -736,28 +736,28 @@ def domDomCongr (σ : ι ≃ ι') (f : M [Λ^ι]→ₗ[R] N) : M [Λ^ι']→ₗ[
 #align alternating_map.dom_dom_congr_apply AlternatingMap.domDomCongr_apply
 
 @[simp]
-theorem domDomCongr_refl (f : M [Λ^ι]→ₗ[R] N) : f.domDomCongr (Equiv.refl ι) = f := rfl
+theorem domDomCongr_refl (f : M [⋀^ι]→ₗ[R] N) : f.domDomCongr (Equiv.refl ι) = f := rfl
 #align alternating_map.dom_dom_congr_refl AlternatingMap.domDomCongr_refl
 
-theorem domDomCongr_trans (σ₁ : ι ≃ ι') (σ₂ : ι' ≃ ι'') (f : M [Λ^ι]→ₗ[R] N) :
+theorem domDomCongr_trans (σ₁ : ι ≃ ι') (σ₂ : ι' ≃ ι'') (f : M [⋀^ι]→ₗ[R] N) :
     f.domDomCongr (σ₁.trans σ₂) = (f.domDomCongr σ₁).domDomCongr σ₂ :=
   rfl
 #align alternating_map.dom_dom_congr_trans AlternatingMap.domDomCongr_trans
 
 @[simp]
-theorem domDomCongr_zero (σ : ι ≃ ι') : (0 : M [Λ^ι]→ₗ[R] N).domDomCongr σ = 0 :=
+theorem domDomCongr_zero (σ : ι ≃ ι') : (0 : M [⋀^ι]→ₗ[R] N).domDomCongr σ = 0 :=
   rfl
 #align alternating_map.dom_dom_congr_zero AlternatingMap.domDomCongr_zero
 
 @[simp]
-theorem domDomCongr_add (σ : ι ≃ ι') (f g : M [Λ^ι]→ₗ[R] N) :
+theorem domDomCongr_add (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) :
     (f + g).domDomCongr σ = f.domDomCongr σ + g.domDomCongr σ :=
   rfl
 #align alternating_map.dom_dom_congr_add AlternatingMap.domDomCongr_add
 
 @[simp]
 theorem domDomCongr_smul {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N]
-    (σ : ι ≃ ι') (c : S) (f : M [Λ^ι]→ₗ[R] N) :
+    (σ : ι ≃ ι') (c : S) (f : M [⋀^ι]→ₗ[R] N) :
     (c • f).domDomCongr σ = c • f.domDomCongr σ :=
   rfl
 #align alternating_map.dom_dom_congr_smul AlternatingMap.domDomCongr_smul
@@ -766,7 +766,7 @@ theorem domDomCongr_smul {S : Type*} [Monoid S] [DistribMulAction S N] [SMulComm
 
 This is declared separately because it does not work with dot notation. -/
 @[simps apply symm_apply]
-def domDomCongrEquiv (σ : ι ≃ ι') : M [Λ^ι]→ₗ[R] N ≃+ M [Λ^ι']→ₗ[R] N where
+def domDomCongrEquiv (σ : ι ≃ ι') : M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N where
   toFun := domDomCongr σ
   invFun := domDomCongr σ.symm
   left_inv f := by
@@ -786,7 +786,7 @@ variable (S : Type*) [Semiring S] [Module S N] [SMulCommClass R S N]
 
 /-- `AlternatingMap.domDomCongr` as a linear equivalence. -/
 @[simps apply symm_apply]
-def domDomCongrₗ (σ : ι ≃ ι') : M [Λ^ι]→ₗ[R] N ≃ₗ[S] M [Λ^ι']→ₗ[R] N where
+def domDomCongrₗ (σ : ι ≃ ι') : M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι']→ₗ[R] N where
   toFun := domDomCongr σ
   invFun := domDomCongr σ.symm
   left_inv f := by ext; simp [Function.comp]
@@ -797,14 +797,14 @@ def domDomCongrₗ (σ : ι ≃ ι') : M [Λ^ι]→ₗ[R] N ≃ₗ[S] M [Λ^ι']
 
 @[simp]
 theorem domDomCongrₗ_refl :
-    (domDomCongrₗ S (Equiv.refl ι) : M [Λ^ι]→ₗ[R] N ≃ₗ[S] M [Λ^ι]→ₗ[R] N) =
+    (domDomCongrₗ S (Equiv.refl ι) : M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι]→ₗ[R] N) =
       LinearEquiv.refl _ _ :=
   rfl
 #align alternating_map.dom_dom_lcongr_refl AlternatingMap.domDomCongrₗ_refl
 
 @[simp]
 theorem domDomCongrₗ_toAddEquiv (σ : ι ≃ ι') :
-    (↑(domDomCongrₗ S σ : M [Λ^ι]→ₗ[R] N ≃ₗ[S] _) : M [Λ^ι]→ₗ[R] N ≃+ _) =
+    (↑(domDomCongrₗ S σ : M [⋀^ι]→ₗ[R] N ≃ₗ[S] _) : M [⋀^ι]→ₗ[R] N ≃+ _) =
       domDomCongrEquiv σ :=
   rfl
 #align alternating_map.dom_dom_lcongr_to_add_equiv AlternatingMap.domDomCongrₗ_toAddEquiv
@@ -813,15 +813,15 @@ end DomDomLcongr
 
 /-- The results of applying `domDomCongr` to two maps are equal if and only if those maps are. -/
 @[simp]
-theorem domDomCongr_eq_iff (σ : ι ≃ ι') (f g : M [Λ^ι]→ₗ[R] N) :
+theorem domDomCongr_eq_iff (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) :
     f.domDomCongr σ = g.domDomCongr σ ↔ f = g :=
-  (domDomCongrEquiv σ : _ ≃+ M [Λ^ι']→ₗ[R] N).apply_eq_iff_eq
+  (domDomCongrEquiv σ : _ ≃+ M [⋀^ι']→ₗ[R] N).apply_eq_iff_eq
 #align alternating_map.dom_dom_congr_eq_iff AlternatingMap.domDomCongr_eq_iff
 
 @[simp]
-theorem domDomCongr_eq_zero_iff (σ : ι ≃ ι') (f : M [Λ^ι]→ₗ[R] N) :
+theorem domDomCongr_eq_zero_iff (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) :
     f.domDomCongr σ = 0 ↔ f = 0 :=
-  (domDomCongrEquiv σ : M [Λ^ι]→ₗ[R] N ≃+ M [Λ^ι']→ₗ[R] N).map_eq_zero_iff
+  (domDomCongrEquiv σ : M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N).map_eq_zero_iff
 #align alternating_map.dom_dom_congr_eq_zero_iff AlternatingMap.domDomCongr_eq_zero_iff
 
 theorem domDomCongr_perm [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) :
@@ -839,7 +839,7 @@ end DomDomCongr
 
 /-- If the arguments are linearly dependent then the result is `0`. -/
 theorem map_linearDependent {K : Type*} [Ring K] {M : Type*} [AddCommGroup M] [Module K M]
-    {N : Type*} [AddCommGroup N] [Module K N] [NoZeroSMulDivisors K N] (f : M [Λ^ι]→ₗ[K] N)
+    {N : Type*} [AddCommGroup N] [Module K N] [NoZeroSMulDivisors K N] (f : M [⋀^ι]→ₗ[K] N)
     (v : ι → M) (h : ¬LinearIndependent K v) : f v = 0 := by
   obtain ⟨s, g, h, i, hi, hz⟩ := not_linearIndependent_iff.mp h
   letI := Classical.decEq ι
@@ -861,13 +861,13 @@ section Fin
 open Fin
 
 /-- A version of `MultilinearMap.cons_add` for `AlternatingMap`. -/
-theorem map_vecCons_add {n : ℕ} (f : M [Λ^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M) :
+theorem map_vecCons_add {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M) :
     f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m) :=
   f.toMultilinearMap.cons_add _ _ _
 #align alternating_map.map_vec_cons_add AlternatingMap.map_vecCons_add
 
 /-- A version of `MultilinearMap.cons_smul` for `AlternatingMap`. -/
-theorem map_vecCons_smul {n : ℕ} (f : M [Λ^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R)
+theorem map_vecCons_smul {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R)
     (x : M) : f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m) :=
   f.toMultilinearMap.cons_smul _ _ _
 #align alternating_map.map_vec_cons_smul AlternatingMap.map_vecCons_smul
@@ -897,7 +897,7 @@ private theorem alternization_map_eq_zero_of_eq_aux (m : MultilinearMap R (fun _
 
 /-- Produce an `AlternatingMap` out of a `MultilinearMap`, by summing over all argument
 permutations. -/
-def alternatization : MultilinearMap R (fun _ : ι => M) N' →+ M [Λ^ι]→ₗ[R] N' where
+def alternatization : MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N' where
   toFun m :=
     { ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ with
       toFun := ⇑(∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ)
@@ -934,7 +934,7 @@ namespace AlternatingMap
 
 /-- Alternatizing a multilinear map that is already alternating results in a scale factor of `n!`,
 where `n` is the number of inputs. -/
-theorem coe_alternatization [DecidableEq ι] [Fintype ι] (a : M [Λ^ι]→ₗ[R] N') :
+theorem coe_alternatization [DecidableEq ι] [Fintype ι] (a : M [⋀^ι]→ₗ[R] N') :
     MultilinearMap.alternatization (a : MultilinearMap R (fun _ => M) N')
     = Nat.factorial (Fintype.card ι) • a := by
   apply AlternatingMap.coe_injective
@@ -972,7 +972,7 @@ variable [Module R' N₁] [Module R' N₂]
 
 /-- Two alternating maps indexed by a `Fintype` are equal if they are equal when all arguments
 are distinct basis vectors. -/
-theorem Basis.ext_alternating {f g : N₁ [Λ^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁)
+theorem Basis.ext_alternating {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁)
     (h : ∀ v : ι → ι₁, Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) :
     f = g := by
   classical
@@ -1004,8 +1004,8 @@ It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedg
 This is `MultilinearMap.curryLeft` for `AlternatingMap`. See also
 `AlternatingMap.curryLeftLinearMap`. -/
 @[simps]
-def curryLeft {n : ℕ} (f : M'' [Λ^Fin n.succ]→ₗ[R'] N'') :
-    M'' →ₗ[R'] M'' [Λ^Fin n]→ₗ[R'] N'' where
+def curryLeft {n : ℕ} (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
+    M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N'' where
   toFun m :=
     { f.toMultilinearMap.curryLeft m with
       toFun := fun v => f (Matrix.vecCons m v)
@@ -1018,18 +1018,18 @@ def curryLeft {n : ℕ} (f : M'' [Λ^Fin n.succ]→ₗ[R'] N'') :
 #align alternating_map.curry_left_apply_apply AlternatingMap.curryLeft_apply_apply
 
 @[simp]
-theorem curryLeft_zero {n : ℕ} : curryLeft (0 : M'' [Λ^Fin n.succ]→ₗ[R'] N'') = 0 :=
+theorem curryLeft_zero {n : ℕ} : curryLeft (0 : M'' [⋀^Fin n.succ]→ₗ[R'] N'') = 0 :=
   rfl
 #align alternating_map.curry_left_zero AlternatingMap.curryLeft_zero
 
 @[simp]
-theorem curryLeft_add {n : ℕ} (f g : M'' [Λ^Fin n.succ]→ₗ[R'] N'') :
+theorem curryLeft_add {n : ℕ} (f g : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
     curryLeft (f + g) = curryLeft f + curryLeft g :=
   rfl
 #align alternating_map.curry_left_add AlternatingMap.curryLeft_add
 
 @[simp]
-theorem curryLeft_smul {n : ℕ} (r : R') (f : M'' [Λ^Fin n.succ]→ₗ[R'] N'') :
+theorem curryLeft_smul {n : ℕ} (r : R') (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
     curryLeft (r • f) = r • curryLeft f :=
   rfl
 #align alternating_map.curry_left_smul AlternatingMap.curryLeft_smul
@@ -1038,7 +1038,7 @@ theorem curryLeft_smul {n : ℕ} (r : R') (f : M'' [Λ^Fin n.succ]→ₗ[R'] N''
 does not work for this version. -/
 @[simps]
 def curryLeftLinearMap {n : ℕ} :
-    (M'' [Λ^Fin n.succ]→ₗ[R'] N'') →ₗ[R'] M'' →ₗ[R'] M'' [Λ^Fin n]→ₗ[R'] N'' where
+    (M'' [⋀^Fin n.succ]→ₗ[R'] N'') →ₗ[R'] M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N'' where
   toFun f := f.curryLeft
   map_add' := curryLeft_add
   map_smul' := curryLeft_smul
@@ -1047,21 +1047,21 @@ def curryLeftLinearMap {n : ℕ} :
 
 /-- Currying with the same element twice gives the zero map. -/
 @[simp]
-theorem curryLeft_same {n : ℕ} (f : M'' [Λ^Fin n.succ.succ]→ₗ[R'] N'') (m : M'') :
+theorem curryLeft_same {n : ℕ} (f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N'') (m : M'') :
     (f.curryLeft m).curryLeft m = 0 :=
   ext fun x => f.map_eq_zero_of_eq _ (by simp) Fin.zero_ne_one
 #align alternating_map.curry_left_same AlternatingMap.curryLeft_same
 
 @[simp]
 theorem curryLeft_compAlternatingMap {n : ℕ} (g : N'' →ₗ[R'] N₂'')
-    (f : M'' [Λ^Fin n.succ]→ₗ[R'] N'') (m : M'') :
+    (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M'') :
     (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m) :=
   rfl
 #align alternating_map.curry_left_comp_alternating_map AlternatingMap.curryLeft_compAlternatingMap
 
 @[simp]
 theorem curryLeft_compLinearMap {n : ℕ} (g : M₂'' →ₗ[R'] M'')
-    (f : M'' [Λ^Fin n.succ]→ₗ[R'] N'') (m : M₂'') :
+    (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M₂'') :
     (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g :=
   ext fun v => congr_arg f <| funext <| by
     refine' Fin.cases _ _
@@ -1072,7 +1072,7 @@ theorem curryLeft_compLinearMap {n : ℕ} (g : M₂'' →ₗ[R'] M'')
 /-- The space of constant maps is equivalent to the space of maps that are alternating with respect
 to an empty family. -/
 @[simps]
-def constLinearEquivOfIsEmpty [IsEmpty ι] : N'' ≃ₗ[R'] (M'' [Λ^ι]→ₗ[R'] N'') where
+def constLinearEquivOfIsEmpty [IsEmpty ι] : N'' ≃ₗ[R'] (M'' [⋀^ι]→ₗ[R'] N'') where
   toFun := AlternatingMap.constOfIsEmpty R' M'' ι
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
diff --git a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
index 8d3201dec5da5..da6ce16078005 100644
--- a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
+++ b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
@@ -43,7 +43,7 @@ open Equiv
 variable [DecidableEq ιa] [DecidableEq ιb]
 
 /-- summand used in `AlternatingMap.domCoprod` -/
-def domCoprod.summand (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂)
+def domCoprod.summand (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
     (σ : Perm.ModSumCongr ιa ιb) : MultilinearMap R' (fun _ : Sum ιa ιb => Mᵢ) (N₁ ⊗[R'] N₂) :=
   Quotient.liftOn' σ
     (fun σ =>
@@ -66,7 +66,7 @@ def domCoprod.summand (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→
     erw [← a.map_congr_perm fun i => v (σ₁ _), ← b.map_congr_perm fun i => v (σ₁ _)]
 #align alternating_map.dom_coprod.summand AlternatingMap.domCoprod.summand
 
-theorem domCoprod.summand_mk'' (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂)
+theorem domCoprod.summand_mk'' (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
     (σ : Equiv.Perm (Sum ιa ιb)) :
     domCoprod.summand a b (Quotient.mk'' σ) =
       Equiv.Perm.sign σ •
@@ -76,8 +76,8 @@ theorem domCoprod.summand_mk'' (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^
 #align alternating_map.dom_coprod.summand_mk' AlternatingMap.domCoprod.summand_mk''
 
 /-- Swapping elements in `σ` with equal values in `v` results in an addition that cancels -/
-theorem domCoprod.summand_add_swap_smul_eq_zero (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁)
-    (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
+theorem domCoprod.summand_add_swap_smul_eq_zero (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁)
+    (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
     {i j : Sum ιa ιb} (hv : v i = v j) (hij : i ≠ j) :
     domCoprod.summand a b σ v + domCoprod.summand a b (swap i j • σ) v = 0 := by
   refine Quotient.inductionOn' σ fun σ => ?_
@@ -94,8 +94,8 @@ theorem domCoprod.summand_add_swap_smul_eq_zero (a : Mᵢ [Λ^ιa]→ₗ[R'] N
 
 /-- Swapping elements in `σ` with equal values in `v` result in zero if the swap has no effect
 on the quotient. -/
-theorem domCoprod.summand_eq_zero_of_smul_invariant (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁)
-    (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
+theorem domCoprod.summand_eq_zero_of_smul_invariant (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁)
+    (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
     {i j : Sum ιa ιb} (hv : v i = v j) (hij : i ≠ j) :
     swap i j • σ = σ → domCoprod.summand a b σ v = 0 := by
   refine Quotient.inductionOn' σ fun σ => ?_
@@ -154,8 +154,8 @@ The specialized version can be obtained by combining this definition with `finSu
 `LinearMap.mul'`.
 -/
 @[simps]
-def domCoprod (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
-    Mᵢ [Λ^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂) :=
+def domCoprod (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
+    Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂) :=
   { ∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ with
     toFun := fun v => (⇑(∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ)) v
     map_eq_zero_of_eq' := fun v i j hv hij => by
@@ -170,7 +170,7 @@ def domCoprod (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N
 #align alternating_map.dom_coprod AlternatingMap.domCoprod
 #align alternating_map.dom_coprod_apply AlternatingMap.domCoprod_apply
 
-theorem domCoprod_coe (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
+theorem domCoprod_coe (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
     (↑(a.domCoprod b) : MultilinearMap R' (fun _ => Mᵢ) _) =
       ∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ :=
   MultilinearMap.ext fun _ => rfl
@@ -179,8 +179,8 @@ theorem domCoprod_coe (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→
 /-- A more bundled version of `AlternatingMap.domCoprod` that maps
 `((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`. -/
 def domCoprod' :
-    (Mᵢ [Λ^ιa]→ₗ[R'] N₁) ⊗[R'] (Mᵢ [Λ^ιb]→ₗ[R'] N₂) →ₗ[R']
-      (Mᵢ [Λ^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂)) :=
+    (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] (Mᵢ [⋀^ιb]→ₗ[R'] N₂) →ₗ[R']
+      (Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂)) :=
   TensorProduct.lift <| by
     refine'
       LinearMap.mk₂ R' domCoprod (fun m₁ m₂ n => _) (fun c m n => _) (fun m n₁ n₂ => _)
@@ -200,7 +200,7 @@ def domCoprod' :
 #align alternating_map.dom_coprod' AlternatingMap.domCoprod'
 
 @[simp]
-theorem domCoprod'_apply (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
+theorem domCoprod'_apply (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
     domCoprod' (a ⊗ₜ[R'] b) = domCoprod a b :=
   rfl
 #align alternating_map.dom_coprod'_apply AlternatingMap.domCoprod'_apply
@@ -271,7 +271,7 @@ theorem MultilinearMap.domCoprod_alternization [DecidableEq ιa] [DecidableEq ι
 `AlternatingMap`s gives a scaled version of the `AlternatingMap.coprod` of those maps.
 -/
 theorem MultilinearMap.domCoprod_alternization_eq [DecidableEq ιa] [DecidableEq ιb]
-    (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
+    (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
     MultilinearMap.alternatization
       (MultilinearMap.domCoprod a b : MultilinearMap R' (fun _ : Sum ιa ιb => Mᵢ) (N₁ ⊗ N₂)) =
       ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b := by
diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean
index bdb9eacd596c2..60a8af9474368 100644
--- a/Mathlib/LinearAlgebra/Determinant.lean
+++ b/Mathlib/LinearAlgebra/Determinant.lean
@@ -504,7 +504,7 @@ theorem LinearMap.associated_det_comp_equiv {N : Type*} [AddCommGroup N] [Module
 
 /-- The determinant of a family of vectors with respect to some basis, as an alternating
 multilinear map. -/
-nonrec def Basis.det : M [Λ^ι]→ₗ[R] R where
+nonrec def Basis.det : M [⋀^ι]→ₗ[R] R where
   toFun v := det (e.toMatrix v)
   map_add' := by
     intro inst v i x y
@@ -570,7 +570,7 @@ theorem Basis.isUnit_det (e' : Basis ι R M) : IsUnit (e.det e') :=
 
 /-- Any alternating map to `R` where `ι` has the cardinality of a basis equals the determinant
 map with respect to that basis, multiplied by the value of that alternating map on that basis. -/
-theorem AlternatingMap.eq_smul_basis_det (f : M [Λ^ι]→ₗ[R] R) : f = f e • e.det := by
+theorem AlternatingMap.eq_smul_basis_det (f : M [⋀^ι]→ₗ[R] R) : f = f e • e.det := by
   refine' Basis.ext_alternating e fun i h => _
   let σ : Equiv.Perm ι := Equiv.ofBijective i (Finite.injective_iff_bijective.1 h)
   change f (e ∘ σ) = (f e • e.det) (e ∘ σ)
@@ -579,7 +579,7 @@ theorem AlternatingMap.eq_smul_basis_det (f : M [Λ^ι]→ₗ[R] R) : f = f e 
 
 @[simp]
 theorem AlternatingMap.map_basis_eq_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M)
-    (f : M [Λ^ι]→ₗ[R] R) : f e = 0 ↔ f = 0 :=
+    (f : M [⋀^ι]→ₗ[R] R) : f e = 0 ↔ f = 0 :=
   ⟨fun h => by
     cases nonempty_fintype ι
     letI := Classical.decEq ι
@@ -588,7 +588,7 @@ theorem AlternatingMap.map_basis_eq_zero_iff {ι : Type*} [Finite ι] (e : Basis
 #align alternating_map.map_basis_eq_zero_iff AlternatingMap.map_basis_eq_zero_iff
 
 theorem AlternatingMap.map_basis_ne_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M)
-    (f : M [Λ^ι]→ₗ[R] R) : f e ≠ 0 ↔ f ≠ 0 :=
+    (f : M [⋀^ι]→ₗ[R] R) : f e ≠ 0 ↔ f ≠ 0 :=
   not_congr <| f.map_basis_eq_zero_iff e
 #align alternating_map.map_basis_ne_zero_iff AlternatingMap.map_basis_ne_zero_iff
 
diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
index b6c104ce715ad..c62b228966c20 100644
--- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
@@ -295,7 +295,7 @@ variable (R)
 
 This is a special case of `MultilinearMap.mkPiAlgebraFin`, and the exterior algebra version of
 `TensorAlgebra.tprod`. -/
-def ιMulti (n : ℕ) : M [Λ^Fin n]→ₗ[R] ExteriorAlgebra R M :=
+def ιMulti (n : ℕ) : M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M :=
   let F := (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun _ => ι R
   { F with
     map_eq_zero_of_eq' := fun f x y hfxy hxy => by
diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
index c987134cde05d..c7d5a09207509 100644
--- a/Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
+++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
@@ -33,7 +33,7 @@ variable [Module R M] [Module R N] [Module R N']
 
 -- This instance can't be found where it's needed if we don't remind lean that it exists.
 instance AlternatingMap.instModuleAddCommGroup {ι : Type*} :
-    Module R (M [Λ^ι]→ₗ[R] N) := by
+    Module R (M [⋀^ι]→ₗ[R] N) := by
   infer_instance
 #align alternating_map.module_add_comm_group AlternatingMap.instModuleAddCommGroup
 
@@ -43,10 +43,10 @@ open CliffordAlgebra hiding ι
 
 /-- Build a map out of the exterior algebra given a collection of alternating maps acting on each
 exterior power -/
-def liftAlternating : (∀ i, M [Λ^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N := by
+def liftAlternating : (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N := by
   suffices
-    (∀ i, M [Λ^Fin i]→ₗ[R] N) →ₗ[R]
-      ExteriorAlgebra R M →ₗ[R] ∀ i, M [Λ^Fin i]→ₗ[R] N by
+    (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R]
+      ExteriorAlgebra R M →ₗ[R] ∀ i, M [⋀^Fin i]→ₗ[R] N by
     refine' LinearMap.compr₂ this _
     refine' (LinearEquiv.toLinearMap _).comp (LinearMap.proj 0)
     exact AlternatingMap.constLinearEquivOfIsEmpty.symm
@@ -67,7 +67,7 @@ def liftAlternating : (∀ i, M [Λ^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra
 #align exterior_algebra.lift_alternating ExteriorAlgebra.liftAlternating
 
 @[simp]
-theorem liftAlternating_ι (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M) :
+theorem liftAlternating_ι (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (m : M) :
     liftAlternating (R := R) (M := M) (N := N) f (ι R m) = f 1 ![m] := by
   dsimp [liftAlternating]
   rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]
@@ -78,7 +78,7 @@ theorem liftAlternating_ι (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M) :
   rw [Matrix.zero_empty]
 #align exterior_algebra.lift_alternating_ι ExteriorAlgebra.liftAlternating_ι
 
-theorem liftAlternating_ι_mul (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M)
+theorem liftAlternating_ι_mul (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (m : M)
     (x : ExteriorAlgebra R M) :
     liftAlternating (R := R) (M := M) (N := N) f (ι R m * x) =
     liftAlternating (R := R) (M := M) (N := N) (fun i => (f i.succ).curryLeft m) x := by
@@ -88,21 +88,21 @@ theorem liftAlternating_ι_mul (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M)
 #align exterior_algebra.lift_alternating_ι_mul ExteriorAlgebra.liftAlternating_ι_mul
 
 @[simp]
-theorem liftAlternating_one (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) :
+theorem liftAlternating_one (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) :
     liftAlternating (R := R) (M := M) (N := N) f (1 : ExteriorAlgebra R M) = f 0 0 := by
   dsimp [liftAlternating]
   rw [foldl_one]
 #align exterior_algebra.lift_alternating_one ExteriorAlgebra.liftAlternating_one
 
 @[simp]
-theorem liftAlternating_algebraMap (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (r : R) :
+theorem liftAlternating_algebraMap (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (r : R) :
     liftAlternating (R := R) (M := M) (N := N) f (algebraMap _ (ExteriorAlgebra R M) r) =
     r • f 0 0 := by
   rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]
 #align exterior_algebra.lift_alternating_algebra_map ExteriorAlgebra.liftAlternating_algebraMap
 
 @[simp]
-theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [Λ^Fin i]→ₗ[R] N)
+theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [⋀^Fin i]→ₗ[R] N)
     (v : Fin n → M) : liftAlternating (R := R) (M := M) (N := N) f (ιMulti R n v) = f n v := by
   rw [ιMulti_apply]
   -- porting note: `v` is generalized automatically so it was removed from the next line
@@ -118,13 +118,13 @@ theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [Λ^Fin i]→ₗ[R
 #align exterior_algebra.lift_alternating_apply_ι_multi ExteriorAlgebra.liftAlternating_apply_ιMulti
 
 @[simp]
-theorem liftAlternating_comp_ιMulti {n : ℕ} (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) :
+theorem liftAlternating_comp_ιMulti {n : ℕ} (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) :
     (liftAlternating (R := R) (M := M) (N := N) f).compAlternatingMap (ιMulti R n) = f n :=
   AlternatingMap.ext <| liftAlternating_apply_ιMulti f
 #align exterior_algebra.lift_alternating_comp_ι_multi ExteriorAlgebra.liftAlternating_comp_ιMulti
 
 @[simp]
-theorem liftAlternating_comp (g : N →ₗ[R] N') (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) :
+theorem liftAlternating_comp (g : N →ₗ[R] N') (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) :
     (liftAlternating (R := R) (M := M) (N := N') fun i => g.compAlternatingMap (f i)) =
     g ∘ₗ liftAlternating (R := R) (M := M) (N := N) f := by
   ext v
@@ -152,7 +152,7 @@ theorem liftAlternating_ιMulti :
 
 /-- `ExteriorAlgebra.liftAlternating` is an equivalence. -/
 @[simps apply symm_apply]
-def liftAlternatingEquiv : (∀ i, M [Λ^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
+def liftAlternatingEquiv : (∀ i, M [⋀^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
     where
   toFun := liftAlternating (R := R)
   map_add' := map_add _
diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant.lean b/Mathlib/LinearAlgebra/Matrix/Determinant.lean
index b8cda01d065ed..ec2054fed8236 100644
--- a/Mathlib/LinearAlgebra/Matrix/Determinant.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Determinant.lean
@@ -58,7 +58,7 @@ variable {R : Type v} [CommRing R]
 local notation "ε " σ:arg => ((sign σ : ℤ) : R)
 
 /-- `det` is an `AlternatingMap` in the rows of the matrix. -/
-def detRowAlternating : (n → R) [Λ^n]→ₗ[R] R :=
+def detRowAlternating : (n → R) [⋀^n]→ₗ[R] R :=
   MultilinearMap.alternatization ((MultilinearMap.mkPiAlgebra R n R).compLinearMap LinearMap.proj)
 #align matrix.det_row_alternating Matrix.detRowAlternating
 
@@ -91,7 +91,7 @@ theorem det_diagonal {d : n → R} : det (diagonal d) = ∏ i, d i := by
 
 -- @[simp] -- Porting note (#10618): simp can prove this
 theorem det_zero (_ : Nonempty n) : det (0 : Matrix n n R) = 0 :=
-  (detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_zero
+  (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_zero
 #align matrix.det_zero Matrix.det_zero
 
 @[simp]
@@ -240,7 +240,7 @@ theorem det_transpose (M : Matrix n n R) : Mᵀ.det = M.det := by
 /-- Permuting the columns changes the sign of the determinant. -/
 theorem det_permute (σ : Perm n) (M : Matrix n n R) :
     (Matrix.det fun i => M (σ i)) = Perm.sign σ * M.det :=
-  ((detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_perm M σ).trans (by simp [Units.smul_def])
+  ((detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_perm M σ).trans (by simp [Units.smul_def])
 #align matrix.det_permute Matrix.det_permute
 
 /-- Permuting rows and columns with the same equivalence has no effect. -/
@@ -362,7 +362,7 @@ Prove that a matrix with a repeated column has determinant equal to zero.
 
 
 theorem det_eq_zero_of_row_eq_zero {A : Matrix n n R} (i : n) (h : ∀ j, A i j = 0) : det A = 0 :=
-  (detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_coord_zero i (funext h)
+  (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_coord_zero i (funext h)
 #align matrix.det_eq_zero_of_row_eq_zero Matrix.det_eq_zero_of_row_eq_zero
 
 theorem det_eq_zero_of_column_eq_zero {A : Matrix n n R} (j : n) (h : ∀ i, A i j = 0) :
@@ -375,7 +375,7 @@ variable {M : Matrix n n R} {i j : n}
 
 /-- If a matrix has a repeated row, the determinant will be zero. -/
 theorem det_zero_of_row_eq (i_ne_j : i ≠ j) (hij : M i = M j) : M.det = 0 :=
-  (detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_eq_zero_of_eq M hij i_ne_j
+  (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_eq_zero_of_eq M hij i_ne_j
 #align matrix.det_zero_of_row_eq Matrix.det_zero_of_row_eq
 
 /-- If a matrix has a repeated column, the determinant will be zero. -/
@@ -388,7 +388,7 @@ end DetZero
 
 theorem det_updateRow_add (M : Matrix n n R) (j : n) (u v : n → R) :
     det (updateRow M j <| u + v) = det (updateRow M j u) + det (updateRow M j v) :=
-  (detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_add M j u v
+  (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_add M j u v
 #align matrix.det_update_row_add Matrix.det_updateRow_add
 
 theorem det_updateColumn_add (M : Matrix n n R) (j : n) (u v : n → R) :
@@ -399,7 +399,7 @@ theorem det_updateColumn_add (M : Matrix n n R) (j : n) (u v : n → R) :
 
 theorem det_updateRow_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
     det (updateRow M j <| s • u) = s * det (updateRow M j u) :=
-  (detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_smul M j s u
+  (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_smul M j s u
 #align matrix.det_update_row_smul Matrix.det_updateRow_smul
 
 theorem det_updateColumn_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
diff --git a/Mathlib/LinearAlgebra/Orientation.lean b/Mathlib/LinearAlgebra/Orientation.lean
index 176a47e54e220..403458e009469 100644
--- a/Mathlib/LinearAlgebra/Orientation.lean
+++ b/Mathlib/LinearAlgebra/Orientation.lean
@@ -50,7 +50,7 @@ variable (ι ι' : Type*)
 
 /-- An orientation of a module, intended to be used when `ι` is a `Fintype` with the same
 cardinality as a basis. -/
-abbrev Orientation := Module.Ray R (M [Λ^ι]→ₗ[R] R)
+abbrev Orientation := Module.Ray R (M [⋀^ι]→ₗ[R] R)
 #align orientation Orientation
 
 /-- A type class fixing an orientation of a module. -/
@@ -69,7 +69,7 @@ def Orientation.map (e : M ≃ₗ[R] N) : Orientation R M ι ≃ Orientation R N
 #align orientation.map Orientation.map
 
 @[simp]
-theorem Orientation.map_apply (e : M ≃ₗ[R] N) (v : M [Λ^ι]→ₗ[R] R) (hv : v ≠ 0) :
+theorem Orientation.map_apply (e : M ≃ₗ[R] N) (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0) :
     Orientation.map ι e (rayOfNeZero _ v hv) =
       rayOfNeZero _ (v.compLinearMap e.symm) (mt (v.compLinearEquiv_eq_zero_iff e.symm).mp hv) :=
   rfl
@@ -95,7 +95,7 @@ def Orientation.reindex (e : ι ≃ ι') : Orientation R M ι ≃ Orientation R
 #align orientation.reindex Orientation.reindex
 
 @[simp]
-theorem Orientation.reindex_apply (e : ι ≃ ι') (v : M [Λ^ι]→ₗ[R] R) (hv : v ≠ 0) :
+theorem Orientation.reindex_apply (e : ι ≃ ι') (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0) :
     Orientation.reindex R M e (rayOfNeZero _ v hv) =
       rayOfNeZero _ (v.domDomCongr e) (mt (v.domDomCongr_eq_zero_iff e).mp hv) :=
   rfl
@@ -237,7 +237,7 @@ theorem eq_or_eq_neg_of_isEmpty [IsEmpty ι] (o : Orientation R M ι) :
   simp only [ray_eq_iff, sameRay_neg_swap]
   rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]
   intro h
-  set f : (M [Λ^ι]→ₗ[R] R) ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
+  set f : (M [⋀^ι]→ₗ[R] R) ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
   have H : LinearIndependent R ![f x, 1] := by
     convert h.map' f.toLinearMap f.ker
     ext i
diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
index 97fa730bce81e..d509e73ea8536 100644
--- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
+++ b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
@@ -576,12 +576,12 @@ variable [FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (finrank ℝ G = n)]
 /-- The Lebesgue measure associated to an alternating map. It gives measure `|ω v|` to the
 parallelepiped spanned by the vectors `v₁, ..., vₙ`. Note that it is not always a Haar measure,
 as it can be zero, but it is always locally finite and translation invariant. -/
-noncomputable irreducible_def _root_.AlternatingMap.measure (ω : G [Λ^Fin n]→ₗ[ℝ] ℝ) :
+noncomputable irreducible_def _root_.AlternatingMap.measure (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) :
     Measure G :=
   ‖ω (finBasisOfFinrankEq ℝ G _i.out)‖₊ • (finBasisOfFinrankEq ℝ G _i.out).addHaar
 #align alternating_map.measure AlternatingMap.measure
 
-theorem _root_.AlternatingMap.measure_parallelepiped (ω : G [Λ^Fin n]→ₗ[ℝ] ℝ)
+theorem _root_.AlternatingMap.measure_parallelepiped (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ)
     (v : Fin n → G) : ω.measure (parallelepiped v) = ENNReal.ofReal |ω v| := by
   conv_rhs => rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]
   simp only [addHaar_parallelepiped, AlternatingMap.measure, coe_nnreal_smul_apply,
@@ -589,10 +589,10 @@ theorem _root_.AlternatingMap.measure_parallelepiped (ω : G [Λ^Fin n]→ₗ[
     Real.ennnorm_eq_ofReal_abs]
 #align alternating_map.measure_parallelepiped AlternatingMap.measure_parallelepiped
 
-instance (ω : G [Λ^Fin n]→ₗ[ℝ] ℝ) : IsAddLeftInvariant ω.measure := by
+instance (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) : IsAddLeftInvariant ω.measure := by
   rw [AlternatingMap.measure]; infer_instance
 
-instance (ω : G [Λ^Fin n]→ₗ[ℝ] ℝ) : IsLocallyFiniteMeasure ω.measure := by
+instance (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) : IsLocallyFiniteMeasure ω.measure := by
   rw [AlternatingMap.measure]; infer_instance
 
 end
diff --git a/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean b/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean
index 0271a21c6fc6d..48208a41858a4 100644
--- a/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean
@@ -15,7 +15,7 @@ maps, by reusing API about continuous multilinear maps and alternating maps.
 
 ## Notation
 
-`M [Λ^ι]→L[R] N`: notation for `R`-linear continuous alternating maps from `M` to `N`; the arguments
+`M [⋀^ι]→L[R] N`: notation for `R`-linear continuous alternating maps from `M` to `N`; the arguments
 are indexed by `i : ι`.
 
 ## Keywords
@@ -27,7 +27,8 @@ open Function Matrix
 
 open scoped BigOperators
 
-/-- A continuous alternating map is a continuous map from `ι → M` to `N` that is
+/-- A continuous alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→L[R] N`,
+is a continuous map that is
 
 - multilinear : `f (update m i (c • x)) = c • f (update m i x)` and
   `f (update m i (x + y)) = f (update m i x) + f (update m i y)`;
@@ -35,7 +36,7 @@ open scoped BigOperators
 -/
 structure ContinuousAlternatingMap (R M N ι : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
     [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] extends
-    ContinuousMultilinearMap R (fun _ : ι => M) N, M [Λ^ι]→ₗ[R] N where
+    ContinuousMultilinearMap R (fun _ : ι => M) N, M [⋀^ι]→ₗ[R] N where
 
 /-- Projection to `ContinuousMultilinearMap`s. -/
 add_decl_doc ContinuousAlternatingMap.toContinuousMultilinearMap
@@ -43,7 +44,8 @@ add_decl_doc ContinuousAlternatingMap.toContinuousMultilinearMap
 /-- Projection to `AlternatingMap`s. -/
 add_decl_doc ContinuousAlternatingMap.toAlternatingMap
 
-notation M "[Λ^" ι "]→L[" R "]" N:100 => ContinuousAlternatingMap R M N ι
+@[inherit_doc]
+notation M "[⋀^" ι "]→L[" R "]" N:100 => ContinuousAlternatingMap R M N ι
 
 namespace ContinuousAlternatingMap
 
@@ -52,25 +54,25 @@ section Semiring
 variable {R M M' N N' ι : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M]
   [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N]
   [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] {n : ℕ}
-  (f g : M [Λ^ι]→L[R] N)
+  (f g : M [⋀^ι]→L[R] N)
 
 theorem toContinuousMultilinearMap_injective :
     Injective (ContinuousAlternatingMap.toContinuousMultilinearMap :
-      M [Λ^ι]→L[R] N → ContinuousMultilinearMap R (fun _ : ι => M) N)
+      M [⋀^ι]→L[R] N → ContinuousMultilinearMap R (fun _ : ι => M) N)
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
 theorem range_toContinuousMultilinearMap :
     Set.range
         (toContinuousMultilinearMap :
-          M [Λ^ι]→L[R] N → ContinuousMultilinearMap R (fun _ : ι => M) N) =
+          M [⋀^ι]→L[R] N → ContinuousMultilinearMap R (fun _ : ι => M) N) =
       {f | ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0} :=
   Set.ext fun f => ⟨fun ⟨g, hg⟩ => hg ▸ g.2, fun h => ⟨⟨f, h⟩, rfl⟩⟩
 
-instance funLike : FunLike (M [Λ^ι]→L[R] N) (ι → M) N where
+instance funLike : FunLike (M [⋀^ι]→L[R] N) (ι → M) N where
   coe f := f.toFun
   coe_injective' _ _ h := toContinuousMultilinearMap_injective <| DFunLike.ext' h
 
-instance continuousMapClass : ContinuousMapClass (M [Λ^ι]→L[R] N) (ι → M) N where
+instance continuousMapClass : ContinuousMapClass (M [⋀^ι]→L[R] N) (ι → M) N where
   map_continuous f := f.cont
 
 initialize_simps_projections ContinuousAlternatingMap (toFun → apply)
@@ -91,20 +93,20 @@ theorem coe_mk (f : ContinuousMultilinearMap R (fun _ : ι => M) N) (h) : ⇑(mk
 theorem coe_toAlternatingMap : ⇑f.toAlternatingMap = f := rfl
 
 @[ext]
-theorem ext {f g : M [Λ^ι]→L[R] N} (H : ∀ x, f x = g x) : f = g :=
+theorem ext {f g : M [⋀^ι]→L[R] N} (H : ∀ x, f x = g x) : f = g :=
   DFunLike.ext _ _ H
 
-theorem ext_iff {f g : M [Λ^ι]→L[R] N} : f = g ↔ ∀ x, f x = g x :=
+theorem ext_iff {f g : M [⋀^ι]→L[R] N} : f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 
 theorem toAlternatingMap_injective :
-    Injective (toAlternatingMap : (M [Λ^ι]→L[R] N) → (M [Λ^ι]→ₗ[R] N)) := fun f g h =>
+    Injective (toAlternatingMap : (M [⋀^ι]→L[R] N) → (M [⋀^ι]→ₗ[R] N)) := fun f g h =>
   DFunLike.ext' <| by convert DFunLike.ext'_iff.1 h
 
 @[simp]
 theorem range_toAlternatingMap :
-    Set.range (toAlternatingMap : M [Λ^ι]→L[R] N → (M [Λ^ι]→ₗ[R] N)) =
-      {f : M [Λ^ι]→ₗ[R] N | Continuous f} :=
+    Set.range (toAlternatingMap : M [⋀^ι]→L[R] N → (M [⋀^ι]→ₗ[R] N)) =
+      {f : M [⋀^ι]→ₗ[R] N | Continuous f} :=
   Set.ext fun f => ⟨fun ⟨g, hg⟩ => hg ▸ g.cont, fun h => ⟨{ f with cont := h }, DFunLike.ext' rfl⟩⟩
 
 @[simp]
@@ -136,25 +138,25 @@ theorem map_eq_zero_of_not_injective (v : ι → M) (hv : ¬Function.Injective v
 
 /-- Restrict the codomain of a continuous alternating map to a submodule. -/
 @[simps!]
-def codRestrict (f : M [Λ^ι]→L[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) : M [Λ^ι]→L[R] p :=
+def codRestrict (f : M [⋀^ι]→L[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) : M [⋀^ι]→L[R] p :=
   { f.toAlternatingMap.codRestrict p h with toContinuousMultilinearMap := f.1.codRestrict p h }
 
-instance : Zero (M [Λ^ι]→L[R] N) :=
-  ⟨⟨0, (0 : M [Λ^ι]→ₗ[R] N).map_eq_zero_of_eq⟩⟩
+instance : Zero (M [⋀^ι]→L[R] N) :=
+  ⟨⟨0, (0 : M [⋀^ι]→ₗ[R] N).map_eq_zero_of_eq⟩⟩
 
-instance : Inhabited (M [Λ^ι]→L[R] N) :=
+instance : Inhabited (M [⋀^ι]→L[R] N) :=
   ⟨0⟩
 
 @[simp]
-theorem coe_zero : ⇑(0 : M [Λ^ι]→L[R] N) = 0 :=
+theorem coe_zero : ⇑(0 : M [⋀^ι]→L[R] N) = 0 :=
   rfl
 
 @[simp]
-theorem toContinuousMultilinearMap_zero : (0 : M [Λ^ι]→L[R] N).toContinuousMultilinearMap = 0 :=
+theorem toContinuousMultilinearMap_zero : (0 : M [⋀^ι]→L[R] N).toContinuousMultilinearMap = 0 :=
   rfl
 
 @[simp]
-theorem toAlternatingMap_zero : (0 : M [Λ^ι]→L[R] N).toAlternatingMap = 0 :=
+theorem toAlternatingMap_zero : (0 : M [⋀^ι]→L[R] N).toAlternatingMap = 0 :=
   rfl
 
 section SMul
@@ -163,36 +165,36 @@ variable {R' R'' A : Type*} [Monoid R'] [Monoid R''] [Semiring A] [Module A M] [
   [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] [DistribMulAction R'' N]
   [ContinuousConstSMul R'' N] [SMulCommClass A R'' N]
 
-instance : SMul R' (M [Λ^ι]→L[A] N) :=
+instance : SMul R' (M [⋀^ι]→L[A] N) :=
   ⟨fun c f => ⟨c • f.1, (c • f.toAlternatingMap).map_eq_zero_of_eq⟩⟩
 
 @[simp]
-theorem coe_smul (f : M [Λ^ι]→L[A] N) (c : R') : ⇑(c • f) = c • ⇑f :=
+theorem coe_smul (f : M [⋀^ι]→L[A] N) (c : R') : ⇑(c • f) = c • ⇑f :=
   rfl
 
-theorem smul_apply (f : M [Λ^ι]→L[A] N) (c : R') (v : ι → M) : (c • f) v = c • f v :=
+theorem smul_apply (f : M [⋀^ι]→L[A] N) (c : R') (v : ι → M) : (c • f) v = c • f v :=
   rfl
 
 @[simp]
-theorem toContinuousMultilinearMap_smul (c : R') (f : M [Λ^ι]→L[A] N) :
+theorem toContinuousMultilinearMap_smul (c : R') (f : M [⋀^ι]→L[A] N) :
     (c • f).toContinuousMultilinearMap = c • f.toContinuousMultilinearMap :=
   rfl
 
 @[simp]
-theorem toAlternatingMap_smul (c : R') (f : M [Λ^ι]→L[A] N) :
+theorem toAlternatingMap_smul (c : R') (f : M [⋀^ι]→L[A] N) :
     (c • f).toAlternatingMap = c • f.toAlternatingMap :=
   rfl
 
-instance [SMulCommClass R' R'' N] : SMulCommClass R' R'' (M [Λ^ι]→L[A] N) :=
+instance [SMulCommClass R' R'' N] : SMulCommClass R' R'' (M [⋀^ι]→L[A] N) :=
   ⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩
 
-instance [SMul R' R''] [IsScalarTower R' R'' N] : IsScalarTower R' R'' (M [Λ^ι]→L[A] N) :=
+instance [SMul R' R''] [IsScalarTower R' R'' N] : IsScalarTower R' R'' (M [⋀^ι]→L[A] N) :=
   ⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩
 
-instance [DistribMulAction R'ᵐᵒᵖ N] [IsCentralScalar R' N] : IsCentralScalar R' (M [Λ^ι]→L[A] N) :=
+instance [DistribMulAction R'ᵐᵒᵖ N] [IsCentralScalar R' N] : IsCentralScalar R' (M [⋀^ι]→L[A] N) :=
   ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩
 
-instance : MulAction R' (M [Λ^ι]→L[A] N) :=
+instance : MulAction R' (M [⋀^ι]→L[A] N) :=
   toContinuousMultilinearMap_injective.mulAction toContinuousMultilinearMap fun _ _ => rfl
 
 end SMul
@@ -201,7 +203,7 @@ section ContinuousAdd
 
 variable [ContinuousAdd N]
 
-instance : Add (M [Λ^ι]→L[R] N) :=
+instance : Add (M [⋀^ι]→L[R] N) :=
   ⟨fun f g => ⟨f.1 + g.1, (f.toAlternatingMap + g.toAlternatingMap).map_eq_zero_of_eq⟩⟩
 
 @[simp]
@@ -213,29 +215,29 @@ theorem add_apply (v : ι → M) : (f + g) v = f v + g v :=
   rfl
 
 @[simp]
-theorem toContinuousMultilinearMap_add (f g : M [Λ^ι]→L[R] N) : (f + g).1 = f.1 + g.1 :=
+theorem toContinuousMultilinearMap_add (f g : M [⋀^ι]→L[R] N) : (f + g).1 = f.1 + g.1 :=
   rfl
 
 @[simp]
-theorem toAlternatingMap_add (f g : M [Λ^ι]→L[R] N) :
+theorem toAlternatingMap_add (f g : M [⋀^ι]→L[R] N) :
     (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap :=
   rfl
 
-instance addCommMonoid : AddCommMonoid (M [Λ^ι]→L[R] N) :=
+instance addCommMonoid : AddCommMonoid (M [⋀^ι]→L[R] N) :=
   toContinuousMultilinearMap_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
 
 /-- Evaluation of a `ContinuousAlternatingMap` at a vector as an `AddMonoidHom`. -/
-def applyAddHom (v : ι → M) : M [Λ^ι]→L[R] N →+ N :=
+def applyAddHom (v : ι → M) : M [⋀^ι]→L[R] N →+ N :=
   ⟨⟨fun f => f v, rfl⟩, fun _ _ => rfl⟩
 
 @[simp]
-theorem sum_apply {α : Type*} (f : α → M [Λ^ι]→L[R] N) (m : ι → M) {s : Finset α} :
+theorem sum_apply {α : Type*} (f : α → M [⋀^ι]→L[R] N) (m : ι → M) {s : Finset α} :
     (∑ a in s, f a) m = ∑ a in s, f a m :=
   map_sum (applyAddHom m) f s
 
 /-- Projection to `ContinuousMultilinearMap`s as a bundled `AddMonoidHom`. -/
 @[simps]
-def toMultilinearAddHom : M [Λ^ι]→L[R] N →+ ContinuousMultilinearMap R (fun _ : ι => M) N :=
+def toMultilinearAddHom : M [⋀^ι]→L[R] N →+ ContinuousMultilinearMap R (fun _ : ι => M) N :=
   ⟨⟨fun f => f.1, rfl⟩, fun _ _ => rfl⟩
 
 end ContinuousAdd
@@ -249,24 +251,24 @@ def toContinuousLinearMap [DecidableEq ι] (m : ι → M) (i : ι) : M →L[R] N
 
 /-- The cartesian product of two continuous alternating maps, as a continuous alternating map. -/
 @[simps!]
-def prod (f : M [Λ^ι]→L[R] N) (g : M [Λ^ι]→L[R] N') : M [Λ^ι]→L[R] (N × N') :=
+def prod (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') : M [⋀^ι]→L[R] (N × N') :=
   ⟨f.1.prod g.1, (f.toAlternatingMap.prod g.toAlternatingMap).map_eq_zero_of_eq⟩
 
 /-- Combine a family of continuous alternating maps with the same domain and codomains `M' i` into a
 continuous alternating map taking values in the space of functions `Π i, M' i`. -/
 def pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)]
-    [∀ i, Module R (M' i)] (f : ∀ i, M [Λ^ι]→L[R] M' i) : M [Λ^ι]→L[R] ∀ i, M' i :=
+    [∀ i, Module R (M' i)] (f : ∀ i, M [⋀^ι]→L[R] M' i) : M [⋀^ι]→L[R] ∀ i, M' i :=
   ⟨ContinuousMultilinearMap.pi fun i => (f i).1,
     (AlternatingMap.pi fun i => (f i).toAlternatingMap).map_eq_zero_of_eq⟩
 
 @[simp]
 theorem coe_pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
-    [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)] (f : ∀ i, M [Λ^ι]→L[R] M' i) :
+    [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)] (f : ∀ i, M [⋀^ι]→L[R] M' i) :
     ⇑(pi f) = fun m j => f j m :=
   rfl
 
 theorem pi_apply {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
-    [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)] (f : ∀ i, M [Λ^ι]→L[R] M' i) (m : ι → M)
+    [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)] (f : ∀ i, M [⋀^ι]→L[R] M' i) (m : ι → M)
     (j : ι') : pi f m j = f j m :=
   rfl
 
@@ -278,7 +280,7 @@ variable (R M N)
 and continuous 1-multilinear alternating maps from `M` to `N`. -/
 @[simps! apply_apply symm_apply_apply apply_toContinuousMultilinearMap]
 def ofSubsingleton [Subsingleton ι] (i : ι) :
-    (M →L[R] N) ≃ M [Λ^ι]→L[R] N where
+    (M →L[R] N) ≃ M [⋀^ι]→L[R] N where
   toFun f :=
     { AlternatingMap.ofSubsingleton R M N i f with
       toContinuousMultilinearMap := ContinuousMultilinearMap.ofSubsingleton R M N i f }
@@ -296,7 +298,7 @@ variable (ι) {N}
 
 /-- The constant map is alternating when `ι` is empty. -/
 @[simps! toContinuousMultilinearMap apply]
-def constOfIsEmpty [IsEmpty ι] (m : N) : M [Λ^ι]→L[R] N :=
+def constOfIsEmpty [IsEmpty ι] (m : N) : M [⋀^ι]→L[R] N :=
   { AlternatingMap.constOfIsEmpty R M ι m with
     toContinuousMultilinearMap := ContinuousMultilinearMap.constOfIsEmpty R (fun _ => M) m }
 
@@ -309,31 +311,31 @@ end
 
 /-- If `g` is continuous alternating and `f` is a continuous linear map, then `g (f m₁, ..., f mₙ)`
 is again a continuous alternating map, that we call `g.compContinuousLinearMap f`. -/
-def compContinuousLinearMap (g : M [Λ^ι]→L[R] N) (f : M' →L[R] M) : M' [Λ^ι]→L[R] N :=
+def compContinuousLinearMap (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) : M' [⋀^ι]→L[R] N :=
   { g.toAlternatingMap.compLinearMap (f : M' →ₗ[R] M) with
     toContinuousMultilinearMap := g.1.compContinuousLinearMap fun _ => f }
 
 @[simp]
-theorem compContinuousLinearMap_apply (g : M [Λ^ι]→L[R] N) (f : M' →L[R] M) (m : ι → M') :
+theorem compContinuousLinearMap_apply (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) (m : ι → M') :
     g.compContinuousLinearMap f m = g (f ∘ m) :=
   rfl
 
 /-- Composing a continuous alternating map with a continuous linear map gives again a
 continuous alternating map. -/
-def _root_.ContinuousLinearMap.compContinuousAlternatingMap (g : N →L[R] N') (f : M [Λ^ι]→L[R] N) :
-    M [Λ^ι]→L[R] N' :=
+def _root_.ContinuousLinearMap.compContinuousAlternatingMap (g : N →L[R] N') (f : M [⋀^ι]→L[R] N) :
+    M [⋀^ι]→L[R] N' :=
   { (g : N →ₗ[R] N').compAlternatingMap f.toAlternatingMap with
     toContinuousMultilinearMap := g.compContinuousMultilinearMap f.1 }
 
 @[simp]
 theorem _root_.ContinuousLinearMap.compContinuousAlternatingMap_coe (g : N →L[R] N')
-    (f : M [Λ^ι]→L[R] N) : ⇑(g.compContinuousAlternatingMap f) = g ∘ f :=
+    (f : M [⋀^ι]→L[R] N) : ⇑(g.compContinuousAlternatingMap f) = g ∘ f :=
   rfl
 
 /-- A continuous linear equivalence of domains defines an equivalence between continuous
 alternating maps. -/
 def _root_.ContinuousLinearEquiv.continuousAlternatingMapComp (e : M ≃L[R] M') :
-    M [Λ^ι]→L[R] N ≃ M' [Λ^ι]→L[R] N where
+    M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N where
   toFun f := f.compContinuousLinearMap ↑e.symm
   invFun f := f.compContinuousLinearMap ↑e
   left_inv f := by ext; simp [(· ∘ ·)]
@@ -342,7 +344,7 @@ def _root_.ContinuousLinearEquiv.continuousAlternatingMapComp (e : M ≃L[R] M')
 /-- A continuous linear equivalence of codomains defines an equivalence between continuous
 alternating maps. -/
 def _root_.ContinuousLinearEquiv.compContinuousAlternatingMap (e : N ≃L[R] N') :
-    M [Λ^ι]→L[R] N ≃ M [Λ^ι]→L[R] N' where
+    M [⋀^ι]→L[R] N ≃ M [⋀^ι]→L[R] N' where
   toFun := (e : N →L[R] N').compContinuousAlternatingMap
   invFun := (e.symm : N' →L[R] N).compContinuousAlternatingMap
   left_inv f := by ext; simp [(· ∘ ·)]
@@ -350,19 +352,19 @@ def _root_.ContinuousLinearEquiv.compContinuousAlternatingMap (e : N ≃L[R] N')
 
 @[simp]
 theorem _root_.ContinuousLinearEquiv.compContinuousAlternatingMap_coe
-    (e : N ≃L[R] N') (f : M [Λ^ι]→L[R] N) : ⇑(e.compContinuousAlternatingMap f) = e ∘ f :=
+    (e : N ≃L[R] N') (f : M [⋀^ι]→L[R] N) : ⇑(e.compContinuousAlternatingMap f) = e ∘ f :=
   rfl
 
 /-- Continuous linear equivalences between domains and codomains define an equivalence between the
 spaces of continuous alternating maps. -/
 def _root_.ContinuousLinearEquiv.continuousAlternatingMapCongr (e : M ≃L[R] M') (e' : N ≃L[R] N') :
-    M [Λ^ι]→L[R] N ≃ M' [Λ^ι]→L[R] N' :=
+    M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N' :=
   e.continuousAlternatingMapComp.trans e'.compContinuousAlternatingMap
 
 /-- `ContinuousAlternatingMap.pi` as an `Equiv`. -/
 @[simps]
 def piEquiv {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, TopologicalSpace (N i)]
-    [∀ i, Module R (N i)] : (∀ i, M [Λ^ι]→L[R] N i) ≃ M [Λ^ι]→L[R] ∀ i, N i where
+    [∀ i, Module R (N i)] : (∀ i, M [⋀^ι]→L[R] N i) ≃ M [⋀^ι]→L[R] ∀ i, N i where
   toFun := pi
   invFun f i := (ContinuousLinearMap.proj i : _ →L[R] N i).compContinuousAlternatingMap f
   left_inv f := by ext; rfl
@@ -437,11 +439,11 @@ variable {A : Type*} [Semiring A] [SMul R A] [Module A M] [Module A N] [IsScalar
 
 /-- Reinterpret a continuous `A`-alternating map as a continuous `R`-alternating map, if `A` is an
 algebra over `R` and their actions on all involved modules agree with the action of `R` on `A`. -/
-def restrictScalars (f : M [Λ^ι]→L[A] N) : M [Λ^ι]→L[R] N :=
+def restrictScalars (f : M [⋀^ι]→L[A] N) : M [⋀^ι]→L[R] N :=
   { f with toContinuousMultilinearMap := f.1.restrictScalars R }
 
 @[simp]
-theorem coe_restrictScalars (f : M [Λ^ι]→L[A] N) : ⇑(f.restrictScalars R) = f :=
+theorem coe_restrictScalars (f : M [⋀^ι]→L[A] N) : ⇑(f.restrictScalars R) = f :=
   rfl
 
 end RestrictScalar
@@ -453,7 +455,7 @@ section Ring
 variable {R M M' N N' ι : Type*} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M]
   [AddCommGroup M'] [Module R M'] [TopologicalSpace M'] [AddCommGroup N] [Module R N]
   [TopologicalSpace N] [AddCommGroup N'] [Module R N'] [TopologicalSpace N'] {n : ℕ}
-  (f g : M [Λ^ι]→L[R] N)
+  (f g : M [⋀^ι]→L[R] N)
 
 @[simp]
 theorem map_sub [DecidableEq ι] (m : ι → M) (i : ι) (x y : M) :
@@ -464,7 +466,7 @@ section TopologicalAddGroup
 
 variable [TopologicalAddGroup N]
 
-instance : Neg (M [Λ^ι]→L[R] N) :=
+instance : Neg (M [⋀^ι]→L[R] N) :=
   ⟨fun f => { -f.toAlternatingMap with toContinuousMultilinearMap := -f.1 }⟩
 
 @[simp]
@@ -474,7 +476,7 @@ theorem coe_neg : ⇑(-f) = -f :=
 theorem neg_apply (m : ι → M) : (-f) m = -f m :=
   rfl
 
-instance : Sub (M [Λ^ι]→L[R] N) :=
+instance : Sub (M [⋀^ι]→L[R] N) :=
   ⟨fun f g =>
     { f.toAlternatingMap - g.toAlternatingMap with toContinuousMultilinearMap := f.1 - g.1 }⟩
 
@@ -482,7 +484,7 @@ instance : Sub (M [Λ^ι]→L[R] N) :=
 
 theorem sub_apply (m : ι → M) : (f - g) m = f m - g m := rfl
 
-instance : AddCommGroup (M [Λ^ι]→L[R] N) :=
+instance : AddCommGroup (M [⋀^ι]→L[R] N) :=
   toContinuousMultilinearMap_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl)
     (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
 
@@ -495,7 +497,7 @@ section CommSemiring
 variable {R M M' N N' ι : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
   [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N]
   [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] {n : ℕ}
-  (f g : M [Λ^ι]→L[R] N)
+  (f g : M [⋀^ι]→L[R] N)
 
 theorem map_piecewise_smul [DecidableEq ι] (c : ι → R) (m : ι → M) (s : Finset ι) :
     f (s.piecewise (fun i => c i • m i) m) = (∏ i in s, c i) • f m :=
@@ -515,7 +517,7 @@ variable {R A M N ι : Type*} [Monoid R] [Semiring A] [AddCommMonoid M] [AddComm
   [TopologicalSpace M] [TopologicalSpace N] [Module A M] [Module A N] [DistribMulAction R N]
   [ContinuousConstSMul R N] [SMulCommClass A R N]
 
-instance [ContinuousAdd N] : DistribMulAction R (M [Λ^ι]→L[A] N) :=
+instance [ContinuousAdd N] : DistribMulAction R (M [⋀^ι]→L[A] N) :=
   Function.Injective.distribMulAction toMultilinearAddHom
     toContinuousMultilinearMap_injective fun _ _ => rfl
 
@@ -529,7 +531,7 @@ variable {R A M N ι : Type*} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCo
 
 /-- The space of continuous alternating maps over an algebra over `R` is a module over `R`, for the
 pointwise addition and scalar multiplication. -/
-instance : Module R (M [Λ^ι]→L[A] N) :=
+instance : Module R (M [⋀^ι]→L[A] N) :=
   Function.Injective.module _ toMultilinearAddHom toContinuousMultilinearMap_injective fun _ _ =>
     rfl
 
@@ -537,7 +539,7 @@ instance : Module R (M [Λ^ι]→L[A] N) :=
 the corresponding multilinear map. -/
 @[simps]
 def toContinuousMultilinearMapLinear :
-    M [Λ^ι]→L[A] N →ₗ[R] ContinuousMultilinearMap A (fun _ : ι => M) N where
+    M [⋀^ι]→L[A] N →ₗ[R] ContinuousMultilinearMap A (fun _ : ι => M) N where
   toFun := toContinuousMultilinearMap
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
@@ -547,7 +549,7 @@ def toContinuousMultilinearMapLinear :
 def piLinearEquiv {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
     [∀ i, TopologicalSpace (M' i)] [∀ i, ContinuousAdd (M' i)] [∀ i, Module R (M' i)]
     [∀ i, Module A (M' i)] [∀ i, SMulCommClass A R (M' i)] [∀ i, ContinuousConstSMul R (M' i)] :
-    (∀ i, M [Λ^ι]→L[A] M' i) ≃ₗ[R] M [Λ^ι]→L[A] ∀ i, M' i :=
+    (∀ i, M [⋀^ι]→L[A] M' i) ≃ₗ[R] M [⋀^ι]→L[A] ∀ i, M' i :=
   { piEquiv with
     map_add' := fun _ _ => rfl
     map_smul' := fun _ _ => rfl }
@@ -558,12 +560,12 @@ section SMulRight
 
 variable {R A M N ι : Type*} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M]
   [Module R N] [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace N] [ContinuousSMul R N]
-  (f : M [Λ^ι]→L[R] R) (z : N)
+  (f : M [⋀^ι]→L[R] R) (z : N)
 
 /-- Given a continuous `R`-alternating map `f` taking values in `R`, `f.smulRight z` is the
 continuous alternating map sending `m` to `f m • z`. -/
 @[simps! toContinuousMultilinearMap apply]
-def smulRight : M [Λ^ι]→L[R] N :=
+def smulRight : M [⋀^ι]→L[R] N :=
   { f.toAlternatingMap.smulRight z with toContinuousMultilinearMap := f.1.smulRight z }
 
 end SMulRight
@@ -577,7 +579,7 @@ variable {R M M' N N' ι : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M
 
 /-- `ContinuousAlternatingMap.compContinuousLinearMap` as a bundled `LinearMap`. -/
 @[simps]
-def compContinuousLinearMapₗ (f : M →L[R] M') : (M' [Λ^ι]→L[R] N) →ₗ[R] (M [Λ^ι]→L[R] N) where
+def compContinuousLinearMapₗ (f : M →L[R] M') : (M' [⋀^ι]→L[R] N) →ₗ[R] (M [⋀^ι]→L[R] N) where
   toFun g := g.compContinuousLinearMap f
   map_add' g g' := by ext; simp
   map_smul' c g := by ext; simp
@@ -586,7 +588,7 @@ variable (R M N N')
 
 /-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled bilinear map. -/
 def _root_.ContinuousLinearMap.compContinuousAlternatingMapₗ :
-    (N →L[R] N') →ₗ[R] (M [Λ^ι]→L[R] N) →ₗ[R] (M [Λ^ι]→L[R] N') :=
+    (N →L[R] N') →ₗ[R] (M [⋀^ι]→L[R] N) →ₗ[R] (M [⋀^ι]→L[R] N') :=
   LinearMap.mk₂ R ContinuousLinearMap.compContinuousAlternatingMap (fun f₁ f₂ g => rfl)
     (fun c f g => rfl) (fun f g₁ g₂ => by ext1; apply f.map_add) fun c f g => by ext1; simp
 
@@ -602,7 +604,7 @@ variable {R M N ι : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [Topolog
 
 /-- Alternatization of a continuous multilinear map. -/
 @[simps (config := .lemmasOnly) apply_toContinuousMultilinearMap]
-def alternatization : ContinuousMultilinearMap R (fun _ : ι => M) N →+ M [Λ^ι]→L[R] N where
+def alternatization : ContinuousMultilinearMap R (fun _ : ι => M) N →+ M [⋀^ι]→L[R] N where
   toFun f :=
     { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • f.domDomCongr σ
       map_eq_zero_of_eq' := fun v i j hv hne => by