𝕜 : Type ?u.2756723
E : Type ?u.2756726
F : Type ?u.2756729
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), inner (↑S x) x = inner (↑T x) x) ↔ ∀ (x : V), inner (↑(S - T) x) x = 0
𝕜 : Type ?u.2756723
E : Type ?u.2756726
F : Type ?u.2756729
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), inner (↑S x) x = inner (↑T x) x) ↔ S = T
rw [← sub_eq_zero, ← inner_map_self_eq_zero]
𝕜 : Type ?u.2756723
E : Type ?u.2756726
F : Type ?u.2756729
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ inner (↑S x) x = inner (↑T x) x ↔ inner (↑(S - T) x) x = 0
𝕜 : Type ?u.2756723
E : Type ?u.2756726
F : Type ?u.2756729
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), inner (↑S x) x = inner (↑T x) x) ↔ ∀ (x : V), inner (↑(S - T) x) x = 0
refine' forall_congr' fun x => _
no goals
𝕜 : Type ?u.2756723
E : Type ?u.2756726
F : Type ?u.2756729
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ inner (↑S x) x = inner (↑T x) x ↔ inner (↑(S - T) x) x = 0
rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]