Documentation

Mathlib.Algebra.CharZero.Infinite

A characteristic-zero semiring is infinite #

source
instance CharZero.infinite (M : Type u_1) [AddMonoidWithOne M] [CharZero M] :
Infinite M
Equations
  • ⋯ = ⋯