ι : Type ?u.1373375
ι' : Type ?u.1373378
𝕜 : Type ?u.1373381
inst✝⁹ : IsROrC 𝕜
E : Type ?u.1373387
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1373407
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1373445
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : OrthonormalBasis (Fin 2) ℝ F
z : ℂ
⊢ ↑(LinearIsometryEquiv.symm v.repr) (↑orthonormalBasisOneI.repr z) = z.re • ↑v 0 + z.im • ↑v 1
ι : Type ?u.1373375
ι' : Type ?u.1373378
𝕜 : Type ?u.1373381
inst✝⁹ : IsROrC 𝕜
E : Type ?u.1373387
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1373407
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1373445
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : OrthonormalBasis (Fin 2) ℝ F
z : ℂ
⊢ ↑(isometryOfOrthonormal v) z = z.re • ↑v 0 + z.im • ↑v 1
rw [Complex.isometryOfOrthonormal, LinearIsometryEquiv.trans_apply]
no goals
ι : Type ?u.1373375
ι' : Type ?u.1373378
𝕜 : Type ?u.1373381
inst✝⁹ : IsROrC 𝕜
E : Type ?u.1373387
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1373407
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1373445
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : OrthonormalBasis (Fin 2) ℝ F
z : ℂ
⊢ ↑(LinearIsometryEquiv.symm v.repr) (↑orthonormalBasisOneI.repr z) = z.re • ↑v 0 + z.im • ↑v 1
simp [← v.sum_repr_symm]