𝕜 : Type u_1
E : Type u_2
F : Type ?u.1383018
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
r : ℝ
⊢ ↑r * inner x y = ↑(algebraMap ℝ 𝕜) r * inner x y
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1383018
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
r : ℝ
⊢ inner (↑r • x) y = r • inner x y
rw [inner_smul_left, conj_ofReal, Algebra.smul_def]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1383018
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
r : ℝ
⊢ ↑r * inner x y = ↑(algebraMap ℝ 𝕜) r * inner x y
rfl