Theorems · Inductive type · commutative algebra

CharZero

(R : Type u_1) → [AddMonoidWithOne R] → Prop

Typeclass for monoids with characteristic zero. (This is usually stated on fields but it makes sense for any additive monoid with 1.) Warning: for a semiring R, CharZero R and CharP R 0 need not coincide. * CharZero R requires an injection ℕ ↪ R; * CharP R 0 asks that only 0 : ℕ maps to 0 : R under the map ℕ → 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.CharZero.Defs

Cited by

932 results in Mathlib

Foundations

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

Assumes

AddMonoidWithOne