# Documentation

Mathlib.Algebra.CharP.ExpChar

# 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

class inductive ExpChar (R : Type u) [] :

The definition of the exponential characteristic of a semiring.

Instances
theorem expChar_one_of_char_zero (R : Type u) [] (q : ) [hp : CharP R 0] [hq : ExpChar R q] :
q = 1

The exponential characteristic is one if the characteristic is zero.

theorem char_eq_expChar_iff (R : Type u) [] (p : ) (q : ) [hp : CharP R p] [hq : ExpChar R q] :
p = q

The characteristic equals the exponential characteristic iff the former is prime.

theorem char_zero_of_expChar_one (R : Type u) [] [] (p : ) [hp : CharP R p] [hq : ExpChar R 1] :
p = 0

The exponential characteristic is one if the characteristic is zero.

instance charZero_of_expChar_one' (R : Type u) [] [] [hq : ExpChar R 1] :

The characteristic is zero if the exponential characteristic is one.

theorem expChar_one_iff_char_zero (R : Type u) [] [] (p : ) (q : ) [CharP R p] [ExpChar R q] :
q = 1 p = 0

The exponential characteristic is one iff the characteristic is zero.

theorem char_prime_of_ne_zero (R : Type u) [] [] [] {p : } [hp : CharP R p] (p_ne_zero : p 0) :

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

theorem expChar_is_prime_or_one (R : Type u) [] (q : ) [hq : ExpChar R q] :
q = 1

The exponential characteristic is a prime number or one.