mathlib3 documentation

algebra.char_p.exp_char

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 #

Tags #

exponential characteristic, characteristic

@[class]
inductive exp_char (R : Type u) [semiring R] :
Prop

The definition of the exponential characteristic of a semiring.

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.

theorem char_eq_exp_char_iff (R : Type u) [semiring R] (p q : ) [hp : char_p R p] [hq : exp_char R 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 : 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] :
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] [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.