A characteristic-zero semiring is infinite

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

Equations

• CharZero.infinite = CharZero.infinite.proof_1