F : Type ?u.1519076
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedRing γ
inst✝ : NormedAlgebra 𝕜 γ
f g : α →ᵇ γ
x : α
c k : 𝕜
a : α
⊢ ↑(k • 1) a = k • 1
F : Type ?u.1519076
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedRing γ
inst✝ : NormedAlgebra 𝕜 γ
f g : α →ᵇ γ
x : α
c k : 𝕜
a : α
⊢ ↑(↑(algebraMap 𝕜 (α →ᵇ γ)) k) a = k • 1
rw [Algebra.algebraMap_eq_smul_one]
no goals
F : Type ?u.1519076
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedRing γ
inst✝ : NormedAlgebra 𝕜 γ
f g : α →ᵇ γ
x : α
c k : 𝕜
a : α
⊢ ↑(k • 1) a = k • 1
rfl