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

@[deprecated Polynomial.cardinalMk_eq_max (since := "2024-11-10")]

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

Alias of Polynomial.cardinalMk_eq_max.

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

@[deprecated Polynomial.cardinalMk_le_max (since := "2024-11-10")]

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

Alias of Polynomial.cardinalMk_le_max.