Documentation

Mathlib.Algebra.CharZero.Infinite

← Mathematical handbook

A characteristic-zero semiring is infinite #

source
@[instance 100]
instance CharZero.infinite (M : Type u_1) [AddMonoidWithOne M] [CharZero M] :
Infinite M