English
For any ContinuousLinearMap f: E →L E, the scalar series with coefficients (-1)^k c(k) composed with f equals the negated composition, i.e., (ofScalars E c).compContinuousLinearMap (−f) = (ofScalars E (k ↦ (−1)^k c(k))).compContinuousLinearMap f.
Русский
Для любого линейного отображения f: E→E верно, что скалярная серия с коэффициентами (-1)^k c(k), композиция с f, равна отрицательному композиционному отображению.
LaTeX
$$$\big(\operatorname{ofScalars} E c\big) \circ_{\text{cont}} (-f) = \big(\operatorname{ofScalars} E (k \mapsto (-1)^k c(k))\big) \circ_{\text{cont}} f$$$
Lean4
@[simp]
theorem ofScalarsSum_unop [T2Space E] (x : Eᵐᵒᵖ) :
ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x) := by
simp [ofScalars_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]
