Cardinality of Polynomial Ring

The result in this file is that the cardinality of R[X] is at most the maximum of #R and ℵ₀.

@[simp]

theorem Polynomial.cardinalMk_eq_max {R : Type u} [Semiring R] [Nontrivial R] : Cardinal.mk (Polynomial R) = max (Cardinal.mk R) Cardinal.aleph0

theorem Polynomial.cardinalMk_le_max {R : Type u} [Semiring R] : Cardinal.mk (Polynomial R) ≤ max (Cardinal.mk R) Cardinal.aleph0