Commit 2023-05-27 18:17 13b0d72f

feat(measure_theory/function/l1_space): generalize multiplicative results to is_unit (#19073) This generalization lets us use these lemmas for left- and right- multiplication by non-commutative normed rings. This doesn't make it all the way to integral_mul_const, but it's a step in that direction.