𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1357503
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 : F →L[𝕜] E
⊢ ↑adjoint (comp (↑adjoint S) (comp T S)) = comp (↑adjoint S) (comp T S)
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1357503
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 : F →L[𝕜] E
⊢ IsSelfAdjoint (comp (↑adjoint S) (comp T S))
rw [isSelfAdjoint_iff'] at hT⊢
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1357503
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 : F →L[𝕜] E
⊢ comp (comp (↑adjoint S) T) S = comp (↑adjoint S) (comp T S)
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1357503
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 : F →L[𝕜] E
⊢ ↑adjoint (comp (↑adjoint S) (comp T S)) = comp (↑adjoint S) (comp T S)
simp only [hT, adjoint_comp, adjoint_adjoint]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1357503
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 : F →L[𝕜] E
⊢ comp (comp (↑adjoint S) T) S = comp (↑adjoint S) (comp T S)
exact ContinuousLinearMap.comp_assoc _ _ _