Commit 2024-06-16 12:04 950e3d06
View on Github →feat (MeasureTheory/Function): trivial cases of integrability / summability (#13872) Any function on a finite type is multipliable / summable; a function on a discrete measurable space is integrable iff its norm is summable.