conj_adjoint — Mathlib

English

If T is self-adjoint, then S ∘L T ∘L S.adjoint is self-adjoint for any S.

Русский

Если T самосопряжён, то S ∘L T ∘L S.adjoint самосопряжён для любого S.

LaTeX

$$IsSelfAdjoint T \rightarrow IsSelfAdjoint (S \circL T \circL S.adjoint)$$

Lean4

/-- Conjugating preserves self-adjointness. -/
theorem conj_adjoint {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : E →L[𝕜] F) : IsSelfAdjoint (S ∘L T ∘L S.adjoint) :=
  by
  rw [isSelfAdjoint_iff'] at hT ⊢
  simp only [hT, adjoint_comp, adjoint_adjoint]
  exact ContinuousLinearMap.comp_assoc _ _ _

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