feat(topology/instances/ennreal): sum of nonzero constants is infinity (#9294)
feat(topology/instances/ennreal): sum of nonzero constants is infinity (#9294)






leanprover-community/mathlib,leanprover-community/mathlib