𝕜 : Type ?u.2218410
E : Type ?u.2218413
F : Type ?u.2218416
G : Type ?u.2218419
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
E' : Type u_1
F' : Type u_2
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : FiniteDimensional ℝ E'
inst✝ : FiniteDimensional ℝ F'
A : E' →ₗ[ℝ] F'
x : E'
y : F'
⊢ ↑(↑sesqFormOfInner (↑A x)) y = ↑(↑sesqFormOfInner x) (↑(↑adjoint A) y)
𝕜 : Type ?u.2218410
E : Type ?u.2218413
F : Type ?u.2218416
G : Type ?u.2218419
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
E' : Type u_1
F' : Type u_2
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : FiniteDimensional ℝ E'
inst✝ : FiniteDimensional ℝ F'
A : E' →ₗ[ℝ] F'
⊢ IsAdjointPair sesqFormOfInner sesqFormOfInner A (↑adjoint A)
intro x y
no goals
𝕜 : Type ?u.2218410
E : Type ?u.2218413
F : Type ?u.2218416
G : Type ?u.2218419
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
E' : Type u_1
F' : Type u_2
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : FiniteDimensional ℝ E'
inst✝ : FiniteDimensional ℝ F'
A : E' →ₗ[ℝ] F'
x : E'
y : F'
⊢ ↑(↑sesqFormOfInner (↑A x)) y = ↑(↑sesqFormOfInner x) (↑(↑adjoint A) y)
simp only [sesqFormOfInner_apply_apply, adjoint_inner_left]