Structures · Algebra

CharP

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 only 0 : ℕ maps to 0 : 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.

Defined in

Mathlib.Algebra.CharP.Defs

Shape

2 explicit arguments · adds cast_eq_zero_iff