mathlib

7a367f37 - feat(algebra/char_p): add lemma ring_char_ne_one (#2595)

feat(algebra/char_p): add lemma ring_char_ne_one (#2595) This lemma is more useful than the extant `false_of_nonzero_of_char_one` when we are working with the function `ring_char` rather than the `char_p` Prop.