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.cardinal_mk_eq_max
{R : Type u}
[Semiring R]
[Nontrivial R]
:
Cardinal.mk (Polynomial R) = max (Cardinal.mk R) Cardinal.aleph0
theorem
Polynomial.cardinal_mk_le_max
{R : Type u}
[Semiring R]
:
Cardinal.mk (Polynomial R) ≤ max (Cardinal.mk R) Cardinal.aleph0