mathlib3

d06eb858 - 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