mathlib

e3f897c2 - feat(algebra/char_p): characteristic of fraction_ring (#7703)

feat(algebra/char_p): characteristic of fraction_ring (#7703) Adding the characteristics of a `fraction_ring` for an integral domain. Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>