refactor(Vorspiel): rename Matrix.map to Matrix.vecMap to avoid Mathlib clash

Foundation.Vorspiel.Matrix defined its own Matrix.map, a vector map
(Fin k → α) → (Fin k → β), shadowing Mathlib's Matrix.map. Both auto-generate
Matrix.map.eq_1, so importing Foundation alongside any Mathlib module that
materializes Mathlib's Matrix.map.eq_1 (e.g. Bochner integration, matrix-heavy
analysis) fails with an 'environment already contains Matrix.map.eq_1' clash.
Because Vorspiel.Matrix sits in Foundation's prelude, this blocks co-importing
Foundation with large parts of Mathlib.

Rename the def to vecMap. The postfix notation ⨟ and all lemmas are unchanged in
behavior; no qualified Matrix.map (vector) references exist elsewhere in the tree.

Author: A-M-Berns

Foundation/Vorspiel/Matrix.lean

@@ -245,23 +245,26 @@ def foldr (f : α → β → β) (init : β) : {k : ℕ} → (Fin k → α) →
   |     0, _ => init
   | _ + 1, v => f (vecHead v) (Matrix.foldr f init (vecTail v))
 
-def map (f : α → β) : (Fin k → α) → (Fin k → β) := fun v ↦ f ∘ v
+-- Renamed from `Matrix.map` to `Matrix.vecMap` to avoid clashing with Mathlib's
+-- `Matrix.map`: both auto-generate `Matrix.map.eq_1`, which makes Foundation
+-- unimportable alongside Mathlib matrix/analysis theory (e.g. Bochner integration).
+def vecMap (f : α → β) : (Fin k → α) → (Fin k → β) := fun v ↦ f ∘ v
 
 section map
 
-postfix:max "⨟" => map
+postfix:max "⨟" => vecMap
 
 variable (f : α → β)
 
 @[simp] lemma map_nil (v : Fin 0 → α) : f⨟ v = ![] := empty_eq (f⨟ v)
 
 @[simp] lemma map_cons (a : α) (v : Fin k → α) : f⨟ (a :> v) = f a :> f⨟ v := by
   ext i
-  cases i using Fin.cases <;> simp [map]
+  cases i using Fin.cases <;> simp [vecMap]
 
 @[simp] lemma map_cons' (v : Fin (k + 1) → α) : f⨟ v = f (vecHead v) :> f⨟ (vecTail v) := by
   ext i
-  cases i using Fin.cases <;> { simp [map]; rfl }
+  cases i using Fin.cases <;> { simp [vecMap]; rfl }
 
 @[simp] lemma map_app (v : Fin k → α) (i : Fin k) : (f⨟ v) i = f (v i) := rfl