English
Let E be as above and c a sequence of scalars. For a continuous linear map f: E → E, precomposition with -f corresponds to replacing the coefficient sequence by (-1)^k c_k; i.e., composing the scalar-series with -f on the left equals composing with f after replacing coefficients by (-1)^k c_k.
Русский
Пусть E — как выше, и c — последовательность скаляров. Предпоследовательность с -f эквивалентна замене коэффициентной последовательности на (-1)^k c_k; то есть композиция скалярного ряда с -f слева равна композиции со скалярным рядом с коэффициентами (-1)^k c_k и последующим применением f.
LaTeX
$$$ (\\mathrm{ofScalars}\ E\\ c) \\circ (-f) = (\\mathrm{ofScalars}\ E(\\lambda k. (-1)^k c_k)) \\circ f $$$
Lean4
theorem ofScalars_comp_neg (f : E →L[𝕜] E) :
(ofScalars E c).compContinuousLinearMap (-f) = (ofScalars E (fun k ↦ (-1) ^ k * c k)).compContinuousLinearMap f :=
by
conv => lhs; rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]
rw [← FormalMultilinearSeries.compContinuousLinearMap_comp, ofScalars_comp_neg_id]
