Commit 2022-04-10 13:49 6368956a
View on Github →counterexample(counterexamples/char_p_zero_ne_char_zero.lean): char_p R 0 and char_zero R need not coincide (#13080)
Following the Zulip discussion, this counterexample formalizes a semiring R for which char_p R 0 holds, but char_zero R does not.
See #13075 for the PR that lead to this example.