𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.2011794
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
ι : Type u_1
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : (fun x => F) (↑b i)), inner (↑A (↑b i)) y = inner (↑b i) (↑B y)
i : ι
⊢ ↑A (↑b i) = ↑(↑adjoint B) (↑b i)
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.2011794
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
ι : Type u_1
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = ↑adjoint B ↔ ∀ (i : ι) (y : (fun x => F) (↑b i)), inner (↑A (↑b i)) y = inner (↑b i) (↑B y)
refine' ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => Basis.ext b fun i => _⟩
no goals
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.2011794
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
ι : Type u_1
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : (fun x => F) (↑b i)), inner (↑A (↑b i)) y = inner (↑b i) (↑B y)
i : ι
⊢ ↑A (↑b i) = ↑(↑adjoint B) (↑b i)
exact ext_inner_right 𝕜 fun y => by simp only [h i, adjoint_inner_left]
no goals
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.2011794
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
ι : Type u_1
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = ↑adjoint B
x : ι
y : (fun x => F) (↑b x)
⊢ inner (↑A (↑b x)) y = inner (↑b x) (↑B y)
rw [h, adjoint_inner_left]
no goals
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.2011794
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
ι : Type u_1
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : (fun x => F) (↑b i)), inner (↑A (↑b i)) y = inner (↑b i) (↑B y)
i : ι
y : (fun x => F) (↑b i)
⊢ inner (↑A (↑b i)) y = inner (↑(↑adjoint B) (↑b i)) y
simp only [h i, adjoint_inner_left]