feat(topology/algebra/continuous_functions): the ring of continuous functions (#923)
feat(topology/algebra/continuous_functions): the ring of continuous functions (#923)

* feat(topology/algebra/continuous_functions): the ring of continuous functions

* filling in the hierarchy

* use to_additive

leanprover-community/mathlib,leanprover-community/mathlib