Commit 2020-05-05 08:02 7a367f37
View on Github →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.