𝕜 : Type u_1
E : Type u_2
E' : Type ?u.45775
F : Type ?u.45778
G : Type ?u.45781
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner (↑(T + S) x) y = inner x (↑(T + S) y)
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.45775
F : Type ?u.45778
G : Type ?u.45781
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
⊢ IsSymmetric (T + S)
intro x y
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.45775
F : Type ?u.45778
G : Type ?u.45781
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner x (↑T y + ↑S y) = inner x (↑(T + S) y)
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.45775
F : Type ?u.45778
G : Type ?u.45781
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner (↑(T + S) x) y = inner x (↑(T + S) y)
rw [LinearMap.add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right]
no goals
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.45775
F : Type ?u.45778
G : Type ?u.45781
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner x (↑T y + ↑S y) = inner x (↑(T + S) y)
rfl