# Exponential characteristic #

This file defines the exponential characteristic, which is defined to be 1 for a ring with characteristic 0 and the same as the ordinary characteristic, if the ordinary characteristic is prime. This concept is useful to simplify some theorem statements. This file establishes a few basic results relating it to the (ordinary characteristic). The definition is stated for a semiring, but the actual results are for nontrivial rings (as far as exponential characteristic one is concerned), respectively a ring without zero-divisors (for prime characteristic).

## Main results #

`ExpChar`

: the definition of exponential characteristic`expChar_is_prime_or_one`

: the exponential characteristic is a prime or one`char_eq_expChar_iff`

: the characteristic equals the exponential characteristic iff the characteristic is prime

## Tags #

exponential characteristic, characteristic

The exponential characteristic is one if the characteristic is zero.

The characteristic is zero if the exponential characteristic is one.

A helper lemma: the characteristic is prime if it is non-zero.