The generator of the kernel of the unique homomorphism ℕ → R for a semiring R.
Warning: for a semiring R
, CharP R 0
and CharZero R
need not coincide.
CharP R 0
asks that only0 : ℕ
maps to0 : R
under the mapℕ → R
;CharZero R
requires an injectionℕ ↪ R
.
For instance, endowing {0, 1}
with addition given by max
(i.e. 1
is absorbing), shows that
CharZero {0, 1}
does not hold and yet CharP {0, 1} 0
does.
This example is formalized in Counterexamples/CharPZeroNeCharZero.lean
.
Instances
Noncomputable function that outputs the unique characteristic of a semiring.
Equations
Instances For
The characteristic is prime if it is non-zero.
Exponential characteristic #
This section 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).
The definition of the exponential characteristic of a semiring.
- zero: ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], ExpChar R 1
- prime: ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {q : ℕ}, Nat.Prime q → ∀ [hchar : CharP R q], ExpChar R q
Instances
The exponential characteristic is unique.
The exponential characteristic is one if the characteristic is zero.
The characteristic equals the exponential characteristic iff the former is prime.
The exponential characteristic is a prime number or one.
See also CharP.char_is_prime_or_zero
.
The exponential characteristic is positive.
Any power of the exponential characteristic is positive.
Noncomputable function that outputs the unique exponential characteristic of a semiring.
Equations
- ringExpChar R = ringChar R ⊔ 1
Instances For
The exponential characteristic is one if the characteristic is zero.
The characteristic is zero if the exponential characteristic is one.
The exponential characteristic is one iff the characteristic is zero.