Commit 2021-03-18 19:27 aea7dfbc

View on Github →

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.

Estimated changes

Modified src/algebra/char_p/basic.lean

modified theorem char_p.char_is_prime

modified theorem char_p.char_is_prime_of_pos

modified theorem char_p.char_is_prime_of_two_le

modified theorem char_p.char_is_prime_or_zero

modified theorem char_p.char_ne_one