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.

source
@[simp]
theorem counterexample.add_one_eq_one (x : with_zero unit) :
x + 1 = 1
source
theorem counterexample.with_zero_unit_char_p_zero  :
char_p (with_zero unit) 0
source
theorem counterexample.with_zero_unit_not_char_zero  :
¬char_zero (with_zero unit)