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