ofScalars_add — Mathlib

English

The map ofScalars is additive in the coefficient argument: ofScalars E (c + c') = ofScalars E c + ofScalars E c'.

Русский

Отображение скаляров сохраняет сложение по аргументам коэффициентов: ofScalars E (c + c') = ofScalars E c + ofScalars E c'.

LaTeX

$$$\operatorname{ofScalars} E (c + c') = \operatorname{ofScalars} E c + \operatorname{ofScalars} E c'$$$

Lean4

theorem ofScalars_add (c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c' :=
  by
  unfold ofScalars
  simp_rw [Pi.add_apply, Pi.add_def _ _]
  exact funext fun n ↦ Module.add_smul (c n) (c' n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)

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