𝕜 : Type u_2
𝕜₂ : Type ?u.369942
E : Type u_1
F : Type ?u.369948
G : Type ?u.369951
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜₂
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
c : 𝕜
⊢ ‖↑(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖
𝕜 : Type u_2
𝕜₂ : Type ?u.369942
E : Type u_1
F : Type ?u.369948
G : Type ?u.369951
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜₂
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
c : 𝕜
⊢ ‖↑(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖
rw [mul_comm]
no goals
𝕜 : Type u_2
𝕜₂ : Type ?u.369942
E : Type u_1
F : Type ?u.369948
G : Type ?u.369951
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜₂
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
c : 𝕜
⊢ ‖↑(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖
exact norm_smul _ _