English
There is a RingHom C: R →+* C(α, A) sending r to the constant function x ↦ algebraMap_R^A(r).
Русский
Существует кольцевой гомоморфизм C: R →+* C(α, A), отправляющий r в константную функцию x ↦ algebraMap_R^A(r).
LaTeX
$$$\\mathrm{C}: R \\to^{}_{+\\to} C(\\alpha,A), \\quad \\mathrm{C}(r)(x) = \\mathrm{algebraMap}_R^A(r).$$$
Lean4
/-- Continuous constant functions as a `RingHom`. -/
def C : R →+* C(α, A)
where
toFun := fun c : R => ⟨fun _ : α => (algebraMap R A) c, continuous_const⟩
map_one' := by ext _; exact (algebraMap R A).map_one
map_mul' c₁ c₂ := by ext _; exact (algebraMap R A).map_mul _ _
map_zero' := by ext _; exact (algebraMap R A).map_zero
map_add' c₁ c₂ := by ext _; exact (algebraMap R A).map_add _ _
