mathlib

906220ca - feat(topology/bounded_continuous_function): Normed algebra of bounded continuous functions (#2722)

feat(topology/bounded_continuous_function): Normed algebra of bounded continuous functions (#2722) The space `C(α, γ)` of bounded continuous functions into a normed algebra γ is a normed algebra. The space of bounded continuous functions into a normed 𝕜-space is a `C(α, 𝕜)`-module. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>