case h
𝕜 : Type u_3
𝕜₂ : Type ?u.392830
E : Type u_2
F : Type ?u.392836
G : Type ?u.392839
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : SMulCommClass 𝕜 𝕜' E
c : 𝕜'
x : E
⊢ ↑(toSpanSingleton 𝕜 (c • x)) 1 = ↑(c • toSpanSingleton 𝕜 x) 1
𝕜 : Type u_3
𝕜₂ : Type ?u.392830
E : Type u_2
F : Type ?u.392836
G : Type ?u.392839
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : SMulCommClass 𝕜 𝕜' E
c : 𝕜'
x : E
⊢ toSpanSingleton 𝕜 (c • x) = c • toSpanSingleton 𝕜 x
ext1
no goals
case h
𝕜 : Type u_3
𝕜₂ : Type ?u.392830
E : Type u_2
F : Type ?u.392836
G : Type ?u.392839
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : SMulCommClass 𝕜 𝕜' E
c : 𝕜'
x : E
⊢ ↑(toSpanSingleton 𝕜 (c • x)) 1 = ↑(c • toSpanSingleton 𝕜 x) 1
rw [toSpanSingleton_apply, smul_apply, toSpanSingleton_apply, smul_comm]