Commit 2024-05-19 19:30 f4da8e56

feat: BoundedMul class to generalize multiplication of bounded continuous functions. (#12790) Introduce type class BoundedMul, which allows to generalize multiplication of BoundedContinuousFunction to the case where the values are not necessarily in NonUnitalSeminormedRing. The most important case for measure theory applications that is allowed by the generalization is bounded continuous functions with values in ℝ≥0. The instances of Monoid and SemiRing on BoundedContinuousFunction are correspondingly generalized.