# mathlibdocumentation

algebra.char_p.exp_char

# Exponential characteristic #

This file defines the exponential characteristic and 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 #

• exp_char: the definition of exponential characteristic
• exp_char_is_prime_or_one: the exponential characteristic is a prime or one
• char_eq_exp_char_iff: the characteristic equals the exponential characteristic iff the characteristic is prime

## Tags #

exponential characteristic, characteristic

@[class]
inductive exp_char (R : Type u) [semiring R] :
→ Prop
• zero : ∀ {R : Type u} [_inst_2 : semiring R] [_inst_3 : , 1
• prime : ∀ {R : Type u} [_inst_2 : semiring R] {q : }, ∀ [hchar : q], q

The definition of the exponential characteristic of a semiring.

theorem exp_char_one_of_char_zero (R : Type u) [semiring R] (q : ) [hp : 0] [hq : q] :
q = 1

The exponential characteristic is one if the characteristic is zero.

theorem char_eq_exp_char_iff (R : Type u) [semiring R] (p q : ) [hp : p] [hq : q] :
p = q

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

theorem char_zero_of_exp_char_one (R : Type u) [semiring R] [nontrivial R] (p : ) [hp : p] [hq : 1] :
p = 0

The exponential characteristic is one if the characteristic is zero.

@[protected, instance]
def char_zero_of_exp_char_one' (R : Type u) [semiring R] [nontrivial R] [hq : 1] :

The characteristic is zero if the exponential characteristic is one.

theorem exp_char_one_iff_char_zero (R : Type u) [semiring R] [nontrivial R] (p q : ) [ p] [ q] :
q = 1 p = 0

The exponential characteristic is one iff the characteristic is zero.

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

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

theorem exp_char_is_prime_or_one (R : Type u) [semiring R] [nontrivial R] (q : ) [hq : q] :
q = 1

The exponential characteristic is a prime number or one.