English
Let p be a formal multilinear series. If m = n and the inputs v and w agree componentwise (v i = w i for all i with i < m), then p m v = p n w.
Русский
Пусть p — формальная мультилинейная серия. Если m = n и векторы v, w совпадают по компонентам, то p m v = p n w.
LaTeX
$$Eq m n → (∀ i (hi : i < m) (hj : i < n), v ⟨i, hi⟩ = w ⟨i, hj⟩) → p m v = p n w$$
Lean4
/-- Convenience congruence lemma stating in a dependent setting that, if the arguments to a formal
multilinear series are equal, then the values are also equal. -/
theorem congr (p : FormalMultilinearSeries 𝕜 E F) {m n : ℕ} {v : Fin m → E} {w : Fin n → E} (h1 : m = n)
(h2 : ∀ (i : ℕ) (him : i < m) (hin : i < n), v ⟨i, him⟩ = w ⟨i, hin⟩) : p m v = p n w :=
by
subst n
congr with ⟨i, hi⟩
exact h2 i hi hi
