ofScalarsSum_zero

Mathlib.Analysis.Analytic.OfScalars

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

English

The sum evaluated at the zero input satisfies ofScalarsSum c (0) = c(0) • 1.

Русский

Сумма при нулевом аргументе равна c(0) умноженному на единицу: ofScalarsSum c (0) = c(0) • 1.

LaTeX

$$$\operatorname{ofScalarsSum} c (0) = c(0) \cdot 1$$$

Lean4

@[simp]
theorem ofScalarsSum_zero : ofScalarsSum c (0 : E) = c 0 • 1 := by
  simp [ofScalarsSum_eq_tsum, ← ofScalars_apply_eq, ofScalars_apply_zero]

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

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

Разделы

Аффилиация

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