𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1706942
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
x : E
y : F
⊢ inner x (↑↑(↑ContinuousLinearMap.adjoint (↑toContinuousLinearMap ↑(↑toContinuousLinearMap A))) y) =
    inner (↑↑(↑toContinuousLinearMap A) x) y
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1706942
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
x : E
y : F
⊢ inner x (↑(↑adjoint A) y) = inner (↑A x) y
rw [← coe_toContinuousLinearMap A, adjoint_eq_toClm_adjoint]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1706942
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
x : E
y : F
⊢ inner x (↑↑(↑ContinuousLinearMap.adjoint (↑toContinuousLinearMap ↑(↑toContinuousLinearMap A))) y) =
    inner (↑↑(↑toContinuousLinearMap A) x) y
exact ContinuousLinearMap.adjoint_inner_right _ x y