reApplyInnerSelf_smul — Mathlib

English

Generalized statement about scaling: for any c ∈ 𝕜, x ∈ E, T.reApplyInnerSelf (c • x) = ‖c‖^2 · T.reApplyInnerSelf x.

Русский

Обобщенное утверждение о масштабировании: для любого c ∈ 𝕜, x ∈ E, T.reApplyInnerSelf (c • x) = ‖c‖^2 · T.reApplyInnerSelf x.

LaTeX

$$T.reApplyInnerSelf (c • x) = ‖c‖^2 · T.reApplyInnerSelf x$$

Lean4

theorem reApplyInnerSelf_smul (T : E →L[𝕜] E) (x : E) {c : 𝕜} :
    T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x := by
  simp only [ContinuousLinearMap.map_smul, ContinuousLinearMap.reApplyInnerSelf_apply, inner_smul_left,
    inner_smul_right, ← mul_assoc, mul_conj, ← ofReal_pow, ← smul_re, Algebra.smul_def (‖c‖ ^ 2) ⟪T x, x⟫,
    algebraMap_eq_ofReal]

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