𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1322203
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : E →L[𝕜] F
⊢ ↑adjoint (comp S (comp T (↑adjoint S))) = comp S (comp T (↑adjoint S))
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1322203
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : E →L[𝕜] F
⊢ IsSelfAdjoint (comp S (comp T (↑adjoint S)))
rw [isSelfAdjoint_iff'] at hT⊢
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1322203
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : E →L[𝕜] F
⊢ comp (comp S T) (↑adjoint S) = comp S (comp T (↑adjoint S))
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1322203
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : E →L[𝕜] F
⊢ ↑adjoint (comp S (comp T (↑adjoint S))) = comp S (comp T (↑adjoint S))
simp only [hT, adjoint_comp, adjoint_adjoint]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1322203
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : E →L[𝕜] F
⊢ comp (comp S T) (↑adjoint S) = comp S (comp T (↑adjoint S))
exact ContinuousLinearMap.comp_assoc _ _ _