𝕜 : Type u_2
E : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
⊢ ↑(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
⊢ ↑(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
have H : gramSchmidtNormed 𝕜 f i = (‖f i‖⁻¹ : 𝕜) • f i := by
  rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
⊢ gramSchmidtNormed 𝕜 f i ≠ 0
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
⊢ ↑(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
rw [gramSchmidtOrthonormalBasis_apply h, H]
no goals
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
⊢ gramSchmidtNormed 𝕜 f i ≠ 0
simpa [H] using hi
no goals
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
⊢ gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]