Commit 2021-08-31 23:00 065a35dc
View on Github →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.