mathlib

aea7dfbc - chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ (#6753)

chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ (#6753) Taking advantage of the `no_zero_divisors` typeclass, the assumptions on some of the results can be weakened.