mathlib

065a35dc - feat(algebra/{pointwise,algebra/operations}): add `supr_mul` and `mul_supr` (#8923)

feat(algebra/{pointwise,algebra/operations}): add `supr_mul` and `mul_supr` (#8923) Requested by @eric-wieser on Zulip, https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/submodule.2Esupr_mul/near/250122435 and a couple of helper lemmas. Co-authored-by: Eric Wieser wieser.eric@gmail.com Co-authored-by: Eric Wieser <wieser.eric@gmail.com>