𝕜 : Type u_1
E : Type u_2
F : Type ?u.1221416
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y z : E
⊢ ↑(starRingEnd 𝕜) (inner y x) + ↑(starRingEnd 𝕜) (inner z x) = inner x y + inner x z
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1221416
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y z : E
⊢ inner x (y + z) = inner x y + inner x z
rw [← inner_conj_symm, inner_add_left, RingHom.map_add]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1221416
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y z : E
⊢ ↑(starRingEnd 𝕜) (inner y x) + ↑(starRingEnd 𝕜) (inner z x) = inner x y + inner x z
simp only [inner_conj_symm]