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
@[simp]
theorem polynomial.cardinal_mk_eq_max {R : Type u} [semiring R] [nontrivial R] :
cardinal.mk (polynomial R) = linear_order.max (cardinal.mk R) cardinal.aleph_0
source
theorem polynomial.cardinal_mk_le_max {R : Type u} [semiring R] :
cardinal.mk (polynomial R) ≤ linear_order.max (cardinal.mk R) cardinal.aleph_0