ofScalars_smul

Mathlib.Analysis.Analytic.OfScalars

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

English

Scaling inside the coefficients respects the scalar action: ofScalars E (x•c) = x•ofScalars E c.

Русский

Действие скаляра на коэффициенты переносится через ofScalars.

LaTeX

$$$\\text{ofScalars } E (x\\cdot c) = x\\cdot \\text{ofScalars } E c.$$$

Lean4

theorem ofScalars_smul (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c :=
  by
  unfold ofScalars
  simp [Pi.smul_def x _, smul_smul]

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

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

Разделы

Аффилиация

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