English
There is a technical lemma describing how updating one input variable inside a block of a composition affects the resulting multilinear map; the update propagates through the corresponding block index via a defined inverse embedding.
Русский
Существует техническая лемма, описывающая влияние обновления одной входной переменной внутри блока композиции на полученную многолинейную карту; обновление распространяется по соответствующему индексу блока через задаваемое вложение.
LaTeX
$$$p.accordingToUpdate(c,j,v,z)=...$ (describes the exact update rule for applyComposition).$$
Lean4
theorem applyComposition_single (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : 0 < n) (v : Fin n → E) :
p.applyComposition (Composition.single n hn) v = fun _j => p n v :=
by
ext j
refine p.congr (by simp) fun i hi1 hi2 => ?_
dsimp
congr 1
convert Composition.single_embedding hn ⟨i, hi2⟩ using 1
obtain ⟨j_val, j_property⟩ := j
have : j_val = 0 := le_bot_iff.1 (Nat.lt_succ_iff.1 j_property)
congr!
simp
