mathlib3

47e2f804 - chore(*): Replace integral_domain assumptions with no_zero_divisors (#5877)

chore(*): Replace integral_domain assumptions with no_zero_divisors (#5877) This removes unnecessary `nontrivial` assumptions, and reduces some `comm_ring` requirements to `comm_semiring`. This also adds some missing `nontrivial` and `no_zero_divisors` instances. Co-authored-by: Johan Commelin <johan@commelin.net>