mathlib

ac797ad5 - feat(topology/bounded_continuous_function): normed_comm_ring structure on bounded continuous functions (#4326)