feat: vector bundle of ContinuousAlternatingMaps (#35985)

The new file is heavily based on `Hom.lean`, with some theorems removed for now.

Author: urkud

Mathlib.lean

@@ -8017,6 +8017,7 @@ public import Mathlib.Topology.UrysohnsBounded
 public import Mathlib.Topology.UrysohnsLemma
 public import Mathlib.Topology.VectorBundle.Basic
 public import Mathlib.Topology.VectorBundle.Constructions
+public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
 public import Mathlib.Topology.VectorBundle.FiniteDimensional
 public import Mathlib.Topology.VectorBundle.Hom
 public import Mathlib.Topology.VectorBundle.Riemannian

Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

@@ -385,4 +385,10 @@ def continuousAlternatingMapCongr (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] G) :
     (E [⋀^ι]→L[𝕜] F) ≃L[𝕜] (E' [⋀^ι]→L[𝕜] G) :=
   e.continuousAlternatingMapCongrLeft.trans <| e'.continuousAlternatingMapCongrRight
 
+lemma coe_continuousAlternatingMapCongr (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] G) :
+    (e.continuousAlternatingMapCongr e' (ι := ι) : (E [⋀^ι]→L[𝕜] F) →L[𝕜] (E' [⋀^ι]→L[𝕜] G)) =
+      ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 E' F G ι (e' : F →L[𝕜] G) ∘L
+        ContinuousAlternatingMap.compContinuousLinearMapCLM e.symm :=
+  rfl
+
 end ContinuousLinearEquiv