English
Let E be a vector space over a field 𝕜, and let c be a sequence of scalars c: ℕ → 𝕜. The scalar-series operation on FormalMultilinearSeries, when composed with the negation of the identity map, corresponds to a new scalar-series whose k-th coefficient is (-1)^k times the original k-th coefficient. In other words, negating the input linear action flips the parity of the coefficient by (-1)^k.
Русский
Пусть E — векторное пространство над полем 𝕜, и c — последовательность скаляров c: ℕ → 𝕜. Операция скалярных рядов на FormalMultilinearSeries, при композиции с отрицанием тождества, соответствует новой скалярной последовательности, у которой k-й коэффициент равен (-1)^k умножить на исходный коэффициент c_k.
LaTeX
$$$ (\\mathrm{ofScalars}\ E\\ c) \\circ (-\\mathrm{Id}_E) = \\mathrm{ofScalars}_E(\\lambda k. (-1)^k \\; c_k) $$$
Lean4
theorem ofScalars_comp_neg_id :
(ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id _ _) = (ofScalars E (fun k ↦ (-1) ^ k * c k)) :=
by
ext n
rcases n.even_or_odd with (h | h) <;>
simp [ofScalars, show ((-ContinuousLinearMap.id 𝕜 E : _) : E → E) = Neg.neg by rfl, ← List.map_ofFn, h.neg_one_pow]
