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 <837b0bbffcaa89474720fde5011740503a875271@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib