Commit 2022-08-29 08:18 301a6253
View on Github →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.