Theorems · Inductive type · commutative algebra

CharP

(R : Type u_2) → [AddMonoidWithOne R] → outParam ℕ → Prop

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

Cited by

478 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 4 definitions · uses no axioms

Assumes

AddMonoidWithOne