𝕜 : Type u_3
E : Type ?u.2437829
F : Type ?u.2437832
G : Type ?u.2437835
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ∀ (x : EuclideanSpace 𝕜 m) (y : (fun x => EuclideanSpace 𝕜 n) x),
    inner (↑(↑toEuclideanLin Aᴴ) x) y = inner x (↑(↑toEuclideanLin A) y)
𝕜 : Type u_3
E : Type ?u.2437829
F : Type ?u.2437832
G : Type ?u.2437835
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ↑toEuclideanLin Aᴴ = ↑LinearMap.adjoint (↑toEuclideanLin A)
rw [LinearMap.eq_adjoint_iff]
𝕜 : Type u_3
E : Type ?u.2437829
F : Type ?u.2437832
G : Type ?u.2437835
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
x : EuclideanSpace 𝕜 m
y : EuclideanSpace 𝕜 n
⊢ inner (↑(↑toEuclideanLin Aᴴ) x) y = inner x (↑(↑toEuclideanLin A) y)
𝕜 : Type u_3
E : Type ?u.2437829
F : Type ?u.2437832
G : Type ?u.2437835
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ∀ (x : EuclideanSpace 𝕜 m) (y : (fun x => EuclideanSpace 𝕜 n) x),
    inner (↑(↑toEuclideanLin Aᴴ) x) y = inner x (↑(↑toEuclideanLin A) y)
intro x y
no goals
𝕜 : Type u_3
E : Type ?u.2437829
F : Type ?u.2437832
G : Type ?u.2437835
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
x : EuclideanSpace 𝕜 m
y : EuclideanSpace 𝕜 n
⊢ inner (↑(↑toEuclideanLin Aᴴ) x) y = inner x (↑(↑toEuclideanLin A) y)
simp_rw [EuclideanSpace.inner_eq_star_dotProduct, piLp_equiv_toEuclideanLin, toLin'_apply,
  star_mulVec, conjTranspose_conjTranspose, dotProduct_mulVec]