𝕜 : Type ?u.1264931
E : Type ?u.1264934
F : Type ?u.1264937
G : Type ?u.1264940
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 G
inst✝⁶ : CompleteSpace F
E' : Type u_1
F' : Type u_2
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : CompleteSpace E'
inst✝ : CompleteSpace F'
A : E' →L[ℝ] F'
x : E'
y : F'
⊢ ↑(↑sesqFormOfInner (↑↑A x)) y = ↑(↑sesqFormOfInner x) (↑↑(↑adjoint A) y)
𝕜 : Type ?u.1264931
E : Type ?u.1264934
F : Type ?u.1264937
G : Type ?u.1264940
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 G
inst✝⁶ : CompleteSpace F
E' : Type u_1
F' : Type u_2
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : CompleteSpace E'
inst✝ : CompleteSpace F'
A : E' →L[ℝ] F'
⊢ LinearMap.IsAdjointPair sesqFormOfInner sesqFormOfInner ↑A ↑(↑adjoint A)
intro x y
no goals
𝕜 : Type ?u.1264931
E : Type ?u.1264934
F : Type ?u.1264937
G : Type ?u.1264940
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 G
inst✝⁶ : CompleteSpace F
E' : Type u_1
F' : Type u_2
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : CompleteSpace E'
inst✝ : CompleteSpace F'
A : E' →L[ℝ] F'
x : E'
y : F'
⊢ ↑(↑sesqFormOfInner (↑↑A x)) y = ↑(↑sesqFormOfInner x) (↑↑(↑adjoint A) y)
simp only [sesqFormOfInner_apply_apply, adjoint_inner_left, coe_coe]