Theorem: innerSL_smul_comm (ForML/IntegralAgainst.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
c : F
⊢ ((innerSL_smul F x) c) u = ((innerSL_smul F u) c) x
Tactic:
simp [innerSL_smul_apply]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
c : F
⊢ ⟪x, u⟫_ℝ • c = ⟪u, x⟫_ℝ • c

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
c : F
⊢ ⟪x, u⟫_ℝ • c = ⟪u, x⟫_ℝ • c
Tactic:
rw [real_inner_comm]
State after:
no goals