Characteristic of semirings #
The generator of the kernel of the unique homomorphism ℕ → R for a semiring R.
Warning: for a semiring R
, char_p R 0
and char_zero R
need not coincide.
char_p R 0
asks that only0 : ℕ
maps to0 : R
under the mapℕ → R
;char_zero R
requires an injectionℕ ↪ R
.
For instance, endowing {0, 1}
with addition given by max
(i.e. 1
is absorbing), shows that
char_zero {0, 1}
does not hold and yet char_p {0, 1} 0
does.
This example is formalized in counterexamples/char_p_zero_ne_char_zero
.
Instances of this typeclass
- char_p.of_char_zero
- ring_char.char_p
- nat.lcm.char_p
- prod.char_p
- polynomial.char_p
- perfect_closure.char_p
- free_algebra.char_p
- is_fraction_ring.char_p
- char_p.pi
- char_p.pi'
- char_p.subsemiring
- char_p.subring
- char_p.subring'
- zmod.char_p
- matrix.char_p
- galois_field.char_p
- mv_polynomial.char_p
- perfection.char_p
- mod_p.char_p
- pre_tilt.char_p
Noncomputable function that outputs the unique characteristic of a semiring.
Equations
- ring_char R = classical.some _
Instances for ring_char
If ring_char R = 2
, where R
is a finite reduced commutative ring,
then every a : R
is a square.
The characteristic of a finite ring cannot be zero.
We have 2 ≠ 0
in a nontrivial ring whose characteristic is not 2
.
Characteristic ≠ 2
and nontrivial implies that -1 ≠ 1
.
Characteristic ≠ 2
in a domain implies that -a = a
iff a = 0
.
If two integers from {0, 1, -1}
result in equal elements in a ring R
that is nontrivial and of characteristic not 2
, then they are equal.