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.