Structures · Algebra

CharZero

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

Shape

One type argument · adds cast_injective