Commit 2022-06-01 15:09 047db399

feat(algebra/char_p/basic): add lemma ring_char.char_ne_zero_of_finite (#14454) This adds the fact that a finite (not necessarily associative) ring cannot have characteristic zero. See this topic on Zulip.