mathlib documentation

data.polynomial.cardinal

Cardinality of Polynomial Ring #

The reuslt in this file is that the cardinality of polynomial R is at most the maximum of #R and ω.

source
theorem polynomial.cardinal_mk_le_max {R : Type u} [comm_semiring R] :
# R[X] ≤ max (# R) ω