α : Type ?u.431038
β : Type ?u.431041
γ : Type ?u.431044
ι : Type ?u.431047
𝕜 : Type u_2
𝕜' : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖
α : Type ?u.431038
β : Type ?u.431041
γ : Type ?u.431044
ι : Type ?u.431047
𝕜 : Type u_2
𝕜' : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖↑(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖
rw [Algebra.algebraMap_eq_smul_one]
no goals
α : Type ?u.431038
β : Type ?u.431041
γ : Type ?u.431044
ι : Type ?u.431047
𝕜 : Type u_2
𝕜' : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖
exact norm_smul _ _