feat: define continuous alternating maps (#5678)

Mathlib.lean

@@ -3031,6 +3031,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Order
 import Mathlib.Topology.Algebra.InfiniteSum.Real
 import Mathlib.Topology.Algebra.InfiniteSum.Ring
 import Mathlib.Topology.Algebra.Localization
+import Mathlib.Topology.Algebra.Module.Alternating
 import Mathlib.Topology.Algebra.Module.Basic
 import Mathlib.Topology.Algebra.Module.CharacterSpace
 import Mathlib.Topology.Algebra.Module.Determinant

Mathlib/LinearAlgebra/Alternating.lean

@@ -74,7 +74,8 @@ variable (R M N ι)
 /-- An alternating map is a multilinear map that vanishes when two of its arguments are equal.
 -/
 structure AlternatingMap extends MultilinearMap R (fun _ : ι => M) N where
-  map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι) (_ : v i = v j) (_ : i ≠ j), toFun v = 0
+  /-- 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
 
 end
@@ -358,6 +359,11 @@ theorem coe_zero : ((0 : AlternatingMap R M N ι) : MultilinearMap R (fun _ : ι
   rfl
 #align alternating_map.coe_zero AlternatingMap.coe_zero
 
+@[simp]
+theorem mk_zero :
+    mk (0 : MultilinearMap R (fun _ : ι ↦ M) N) (0 : AlternatingMap R M N ι).2 = 0 :=
+  rfl
+
 instance inhabited : Inhabited (AlternatingMap R M N ι) :=
   ⟨0⟩
 #align alternating_map.inhabited AlternatingMap.inhabited