FormalMultilinearSeries.congr

theorem FormalMultilinearSeries.congr : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Ring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalAddGroup F] [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {m n : ℕ} {v : Fin m → E} {w : Fin n → E}, m = n → (∀ (i : ℕ) (him : i < m) (hin : i < n), v ⟨i, him⟩ = w ⟨i, hin⟩) → (p m) v = (p n) w

The theorem `FormalMultilinearSeries.congr` asserts that if we have a formal multilinear series `p` mapping from one topological vector space to another (both over a ring), and if we have two vectors `v` and `w` of possibly different dimensions `m` and `n` that are equal elementwise, then the application of `p` to `v` and `w` will yield the same result, provided `m` equals `n`. This comparison is performed in a dependent type context, ensuring the dimensions of the vectors match the natural numbers with which the multilinear series `p` is indexed.

More concisely: If `p` is a multilinear series mapping topological vector spaces over a ring, and `v` and `w` are vectors of equal dimensions with equal elementwise values, then `p v = p w`.