chore(algebra/ring/defs): refactor `is_domain` (#17721)
Refactor the definiton of `is_domain` to use `is_cancel_mul_zero` instead of `no_zero_divisors`. This is the correct property for a `semiring` (to do in a future refactor).
Corresponding mathlib4 PR https://github.com/leanprover-community/mathlib4/pull/799.
- [x] depends on #17716
