no goals
ι : Type u_1
ι' : Type ?u.777506
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.777535
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.777553
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.777573
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ ↑b.repr v i = inner (↑b i) v
classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
  simp only [one_mul, eq_self_iff_true, map_one]
ι : Type u_1
ι' : Type ?u.777506
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.777535
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.777553
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.777573
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ ↑b.repr v i = ↑(starRingEnd 𝕜) 1 * ↑b.repr v i
ι : Type u_1
ι' : Type ?u.777506
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.777535
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.777553
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.777573
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ ↑b.repr v i = inner (↑b i) v
rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
no goals
ι : Type u_1
ι' : Type ?u.777506
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.777535
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.777553
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.777573
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ ↑b.repr v i = ↑(starRingEnd 𝕜) 1 * ↑b.repr v i
simp only [one_mul, eq_self_iff_true, map_one]