norm_changeOriginSeriesTerm

Mathlib.Analysis.Analytic.ChangeOrigin

URI: https://scilib.ai/kg/mathlib#FormalMultilinearSeries.norm_changeOriginSeriesTerm

← MathLib Explorer

English

The norm of p.changeOriginSeriesTerm equals the norm of p(k+l).

Русский

Норма p.changeOriginSeriesTerm равна норме p(k+l).

LaTeX

$$‖p.changeOriginSeriesTerm k l s hs‖ = ‖p(k+l)‖$$

Lean4

@[simp]
theorem norm_changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
    ‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖ := by
  simp only [changeOriginSeriesTerm, LinearIsometryEquiv.norm_map]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru