applyComposition_ones — Mathlib

English

If p is a formal multilinear series and n>0 with a single block composition, then the n-th coefficient of p∘single is exactly p_n.

Русский

Если p — формальная серия многолинейных коэффициентов, и существует единственный блок композиции, то коэффициент n-ый у p∘single равен p_n.

LaTeX

$$$p.applyComposition(\\mathrm{Composition.single\\}n)\\; v = p(n)\\; v.$$$

Lean4

theorem applyComposition_ones (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) :
    p.applyComposition (Composition.ones n) = fun v i => p 1 fun _ => v (Fin.castLE (Composition.length_le _) i) :=
  by
  funext v i
  apply p.congr (Composition.ones_blocksFun _ _)
  intro j hjn hj1
  obtain rfl : j = 0 := by cutsat
  refine congr_arg v ?_
  rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]

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