English
Two multilinear maps from finite families are equal if they agree on the generators, i.e., the action on elementary coordinate functionals determines the map.
Русский
Две мультилейные отображения из конечных семейств равны, если совпадают на генераторах, то есть на базисных координатных функционалах.
LaTeX
$$$\forall p,\ f\circ\mathrm{LinearMap.single}(p) = g\circ\mathrm{LinearMap.single}(p) \Rightarrow f = g$$$
Lean4
/-- Two multilinear maps from finite families are equal if they agree on the generators.
This is a multilinear version of `LinearMap.pi_ext`. -/
@[ext]
theorem pi_ext [Finite ι] [∀ i, Finite (κ i)] [∀ i, DecidableEq (κ i)]
⦃f g : MultilinearMap R (fun i ↦ Π j : κ i, M i j) N⦄
(h :
∀ p : Π i, κ i,
f.compLinearMap (fun i => LinearMap.single R _ (p i)) = g.compLinearMap (fun i => LinearMap.single R _ (p i))) :
f = g := by
ext x
change f (fun i ↦ x i) = g (fun i ↦ x i)
obtain ⟨i⟩ := nonempty_fintype ι
have (i : _) := (nonempty_fintype (κ i)).some
have := Classical.decEq ι
rw [funext (fun i ↦ Eq.symm (Finset.univ_sum_single (x i)))]
simp_rw [MultilinearMap.map_sum_finset]
congr! 1 with p
simp_rw [MultilinearMap.ext_iff] at h
exact h _ _
