mathlib3

3e067975 - feat(algebra/monoid_algebra/no_zero_divisors): left/right order implies no zero divisors (#16299)

feat(algebra/monoid_algebra/no_zero_divisors): left/right order implies no zero divisors (#16299) This PR is split off from #15983. It contains only the result about zero-divisors in the presence of a left/right-ordered appropriately cancellable semigroup. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315983.20no-zero.20divisors.20and.20right.20orderability)