mathlib

789af09c - feat(algebra/char_p): add two helper lemmas about the cast of the characteristics being zero (#14464)

feat(algebra/char_p): add two helper lemmas about the cast of the characteristics being zero (#14464) - `(ring_char R : R) = 0` and - If there exists a positive `n` lifting to zero, then the characteristics is positive. Co-authored-by: Jon Eugster <eugster.jon@gmail.com>