Cardinality of Multivariate Polynomial Ring #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The main result in this file is mv_polynomial.cardinal_mk_le_max, which says that
the cardinality of mv_polynomial σ R is bounded above by the maximum of #R, #σ
and ℵ₀.
@[simp]
theorem
mv_polynomial.cardinal_mk_eq_max_lift
{σ : Type u}
{R : Type v}
[comm_semiring R]
[nonempty σ]
[nontrivial R] :
@[simp]
theorem
mv_polynomial.cardinal_mk_eq_lift
{σ : Type u}
{R : Type v}
[comm_semiring R]
[is_empty σ] :
cardinal.mk (mv_polynomial σ R) = (cardinal.mk R).lift
theorem
mv_polynomial.cardinal_mk_eq_max
{σ R : Type u}
[comm_semiring R]
[nonempty σ]
[nontrivial R] :
The cardinality of the multivariate polynomial ring, mv_polynomial σ R is at most the maximum
of #R, #σ and ℵ₀