α : Type u_2
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1480657
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
k : R
a : α
⊢ ↑(k • 1) a = k • 1
α : Type u_2
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1480657
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
k : R
a : α
⊢ ↑(↑(algebraMap R C(α, A)) k) a = k • 1
rw [Algebra.algebraMap_eq_smul_one]
no goals
α : Type u_2
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1480657
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
k : R
a : α
⊢ ↑(k • 1) a = k • 1
rfl