Exponential characteristic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

@[class]

inductive exp_char (R : Type u) [semiring R] :

ℕ → Prop

zero : ∀ {R : Type u} [_inst_2 : semiring R] [_inst_3 : char_zero R], exp_char R 1
prime : ∀ {R : Type u} [_inst_2 : semiring R] {q : ℕ}, nat.prime q → ∀ [hchar : char_p R q], exp_char R q

The definition of the exponential characteristic of a semiring.

source

theorem exp_char_one_of_char_zero (R : Type u) [semiring R] (q : ℕ) [hp : char_p R 0] [hq : exp_char R q] :

q = 1

The exponential characteristic is one if the characteristic is zero.

source

theorem char_eq_exp_char_iff (R : Type u) [semiring R] (p q : ℕ) [hp : char_p R p] [hq : exp_char R q] :

p = q ↔ nat.prime p

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

source

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.

source

@[protected, instance]

def char_zero_of_exp_char_one' (R : Type u) [semiring R] [nontrivial R] [hq : exp_char R 1] :

char_zero R

The characteristic is zero if the exponential characteristic is one.

source

theorem exp_char_one_iff_char_zero (R : Type u) [semiring R] [nontrivial R] (p q : ℕ) [char_p R p] [exp_char 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] [no_zero_divisors R] {p : ℕ} [hp : char_p R p] (p_ne_zero : p ≠ 0) :

nat.prime p

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

source

theorem exp_char_is_prime_or_one (R : Type u) [semiring R] [nontrivial R] [no_zero_divisors R] (q : ℕ) [hq : exp_char R q] :

nat.prime q ∨ q = 1

The exponential characteristic is a prime number or one.