mathlib3 documentation

mathlib-counterexamples / char_p_zero_ne_char_zero

char_p R 0 and char_zero R need not coincide for semirings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For rings, the two notions coincide.

In fact, char_p.of_char_zero shows that char_zero R implies char_p R 0 for any char_zero add_monoid R with 1. The reverse implication holds for any add_left_cancel_monoid R with 1, by char_p_to_char_zero.

This file shows that there are semiring R for which char_p R 0 holds and char_zero R does not.

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

@[simp]