mathlib

bd67e852 - feat(algebra/char_p/basic): add ring_char_of_prime_eq_zero (#12024)

feat(algebra/char_p/basic): add ring_char_of_prime_eq_zero (#12024) The characteristic of a ring is `p` if `p` is a prime and `p = 0` in the ring. Co-authored-by: jlh <48520973+Jlh18@users.noreply.github.com>