case h
E : Type ?u.361704
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) z = ↑(x • 1) z
E : Type ?u.361704
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ restrictScalars ℝ (smulRight 1 x) = x • 1
ext1 z
case h
E : Type ?u.361704
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ z * x = x * z
case h
E : Type ?u.361704
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) z = ↑(x • 1) z
dsimp
no goals
case h
E : Type ?u.361704
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ z * x = x * z
apply mul_comm