mathlib

13b0d72f - feat(measure_theory/function/l1_space): generalize multiplicative results to is_unit (#19073)

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.