id_apply_zero

Mathlib.Analysis.Analytic.Composition

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

English

The zero-th coefficient of q.comp p equals q0 evaluated at the zero inputs (identically 0 inputs).

Русский

Нулевой коэффициент q.comp p равен q0 на нулевых входах.

LaTeX

$$$(q.comp p) 0(v) = q 0(v')$ для любых v, v' в нулевом входе.$$

Lean4

@[simp]
theorem id_apply_zero (x : E) (v : Fin 0 → E) : (FormalMultilinearSeries.id 𝕜 E x) 0 v = x :=
  rfl

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

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

Разделы

Аффилиация

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