A characteristic-zero semiring is infinite #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]

def char_zero.infinite (M : Type u_1) [add_monoid_with_one M] [char_zero M] :