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 characteristicexp_char_is_prime_or_one
: the exponential characteristic is a prime or onechar_eq_exp_char_iff
: the characteristic equals the exponential characteristic iff the characteristic is prime
Tags #
exponential characteristic, characteristic
theorem
char_zero_of_exp_char_one
(R : Type u)
[semiring R]
[nontrivial R]
(p : ℕ)
[hp : char_p R p]
[hq : exp_char R 1] :
p = 0
The exponential characteristic is one if the characteristic is zero.
@[protected, instance]
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 : ℕ)
[char_p R p]
[exp_char R q] :
The exponential characteristic is one iff the characteristic is zero.
theorem
char_prime_of_ne_zero
(R : Type u)
[semiring R]
[nontrivial R]
[no_zero_divisors R]
{p : ℕ}
[hp : char_p R 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]
[no_zero_divisors R]
(q : ℕ)
[hq : exp_char R q] :
The exponential characteristic is a prime number or one.