Characteristic zero #
R is called of characteristic zero if every natural number
n is non-zero when considered
as an element of
R. Since this definition doesn't mention the multiplicative structure of
except for the existence of
1 in this file characteristic zero is defined for additive monoids
Main definition #
char_zero is the typeclass of an additive monoid with one such that the natural homomorphism
from the natural numbers into it is injective.
Main statements #
- A linearly ordered semiring has characteristic zero.
- Characteristic zero implies that the additive monoid is infinite.
- Once order of a group is defined for infinite additive monoids redefine or at least connect to
1in the additive monoid with one.
- Unify with
char_p(possibly using an out-parameter)
Typeclass for monoids with characteristic zero. (This is usually stated on fields but it makes sense for any additive monoid with 1.)