mathlib

301a6253 - feat(ring_theory/polynomial/basic): generalize `is_domain` to `no_zero_divisors` (#16226)

feat(ring_theory/polynomial/basic): generalize `is_domain` to `no_zero_divisors` (#16226) This generalization makes this work on `comm_semiring` instead of `comm_ring`. This also removes a duplicate proof of nontriviality. `mv_polynomial.eq_zero_or_eq_zero_of_mul_eq_zero` has been removed in favor of this instance.