removeZero_applyComposition — Mathlib

English

For p a formal multilinear series, q another, and any composition c, updating the input in position j commutes with applying the composition in a precise way: the update on the input translates to an update in the output using the j-th block.

Русский

Для p и q — формальных много-линейных рядов и любой композиции c обновление в позиции j коммутирует с применением композиции: обновление входа превращается в обновление выхода через j-й блок.

LaTeX

$$$p.applyComposition(c, v[ j\\mapsto z]) = \\text{update of } p.applyComposition(c,v) \\, \\text{at } c.index(j).$$$

Lean4

@[simp]
theorem removeZero_applyComposition (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (c : Composition n) :
    p.removeZero.applyComposition c = p.applyComposition c :=
  by
  ext v i
  simp [applyComposition, zero_lt_one.trans_le (c.one_le_blocksFun i), removeZero_of_pos]

Похожие утверждения