ofScalarsSum_op — Mathlib

English

The scalar series composed with the negated identity map equals the scalar series with coefficients (-1)^k c(k) composed with the original linear map, i.e., (ofScalars E c) ∘ (−Id) = ofScalars E (k ↦ (−1)^k c(k)) ∘ Id.

Русский

Скалярная серия после композиции с отрицанием идентичности равна скаляpной серии со скорректированными коэффициентами (-1)^k c(k).

LaTeX

$$$((\operatorname{ofScalars} E c) \circ_{\text{cont}} (-\mathrm{id})) = (\operatorname{ofScalars} E (k \mapsto (-1)^k c(k))) \circ_{\text{cont}} (\mathrm{id})$$$

Lean4

@[simp]
theorem ofScalarsSum_op [T2Space E] (x : E) : ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x) :=
  by simp [ofScalars_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

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