mathlib

f3dbe9f0 - feat(bounded_continuous_function): coe_sum (#6522)

feat(bounded_continuous_function): coe_sum (#6522) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>