mathlib3

6368956a - counterexample(counterexamples/char_p_zero_ne_char_zero.lean): `char_p R 0` and `char_zero R` need not coincide (#13080)

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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F), 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.