𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1665131
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 (↑↑(↑ContinuousLinearMap.adjoint (↑toContinuousLinearMap ↑(↑toContinuousLinearMap A))) y) x =
    inner y (↑↑(↑toContinuousLinearMap A) x)
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1665131
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 (↑(↑adjoint A) y) x = inner y (↑A x)
rw [← coe_toContinuousLinearMap A, adjoint_eq_toClm_adjoint]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1665131
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 (↑↑(↑ContinuousLinearMap.adjoint (↑toContinuousLinearMap ↑(↑toContinuousLinearMap A))) y) x =
    inner y (↑↑(↑toContinuousLinearMap A) x)
exact ContinuousLinearMap.adjoint_inner_left _ x y