unshift_shift — Mathlib

English

If p is a formal multilinear series valued in E →L[𝕜] F, then (p.unshift z).shift = p; the two operations invert each other.

Русский

Пусть p — формальный мультилинейный ряд со значениями в E →L F. Тогда (p.unshift z).shift = p; операции взаимно обратны.

LaTeX

$$$(p.unshift z).\\text{shift} = p$$$

Lean4

theorem unshift_shift {p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {z : F} : (p.unshift z).shift = p :=
  by
  ext1 n
  simp only [shift, Nat.succ_eq_add_one, unshift]
  exact LinearIsometryEquiv.apply_symm_apply (continuousMultilinearCurryRightEquiv' 𝕜 n E F) (p n)

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