CharP R 0 and CharZero R need not coincide for semirings

For rings, the two notions coincide.

In fact, CharP.ofCharZero shows that CharZero R implies CharP R 0 for any CharZero AddMonoid R with 1. The reverse implication holds for any AddLeftCancelMonoid R with 1, by charP_to_charZero.

This file shows that there are semirings R for which CharP R 0 holds and CharZero R does not.

The example is {0, 1} with saturating addition.

@[simp]

theorem Counterexample.add_one_eq_one (x : WithZero Unit) : x + 1 = 1

theorem Counterexample.withZero_unit_charP_zero : CharP (WithZero Unit) 0

theorem Counterexample.withZero_unit_not_charZero : ¬CharZero (WithZero Unit)