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

source

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

ℕ → Prop

zero: ∀ {R : Type u} [inst : Semiring R] [inst_1 : CharZero R], ExpChar R 1
prime: ∀ {R : Type u} [inst : Semiring R] {q : ℕ}, Nat.Prime q → ∀ [hchar : CharP R q], ExpChar R q

The definition of the exponential characteristic of a semiring.

Instances

source

theorem expChar_one_of_char_zero (R : Type u) [Semiring R] (q : ℕ) [hp : CharP R 0] [hq : ExpChar R q] :

q = 1

The exponential characteristic is one if the characteristic is zero.

source

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

p = q ↔ Nat.Prime p

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

source

theorem char_zero_of_expChar_one (R : Type u) [Semiring R] [Nontrivial R] (p : ℕ) [hp : CharP R p] [hq : ExpChar R 1] :

p = 0

The exponential characteristic is one if the characteristic is zero.

source

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

CharZero R

The characteristic is zero if the exponential characteristic is one.

source

theorem expChar_one_iff_char_zero (R : Type u) [Semiring R] [Nontrivial R] (p : ℕ) (q : ℕ) [CharP R p] [ExpChar R q] :

q = 1 ↔ p = 0

The exponential characteristic is one iff the characteristic is zero.

source

theorem char_prime_of_ne_zero (R : Type u) [Semiring R] [Nontrivial R] [NoZeroDivisors R] {p : ℕ} [hp : CharP R p] (p_ne_zero : p ≠ 0) :

Nat.Prime p

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

source

theorem expChar_is_prime_or_one (R : Type u) [Semiring R] (q : ℕ) [hq : ExpChar R q] :

Nat.Prime q ∨ q = 1

The exponential characteristic is a prime number or one.