ofScalars_norm_eq_mul — Mathlib

English

For any continuous linear map f: E → E, the scalar series composed with −f equals the scalar series with coefficients multiplied by (−1)^k, composed with f.

Русский

Для любого непрерывного линейного отображения f: E→E композиция с −f равна серии с коэффициентами, умноженными на (−1)^k, композиция с f.

LaTeX

$$$\big(\operatorname{ofScalars} E c\big).\text{compNeg}(f) = \big(\operatorname{ofScalars} E (k \mapsto (-1)^k c(k))\big).\text{comp}(f)$$$

Lean4

theorem ofScalars_norm_eq_mul : ‖ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ := by
  rw [ofScalars, norm_smul]

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