Cardinality of Multivariate Polynomial Ring

The main result in this file is MvPolynomial.cardinal_mk_le_max, which says that the cardinality of MvPolynomial σ R is bounded above by the maximum of #R, #σ and ℵ₀.

@[simp]

theorem MvPolynomial.cardinal_mk_eq_max_lift {σ : Type u} {R : Type v} [CommSemiring R] [Nonempty σ] [Nontrivial R] : Cardinal.mk (MvPolynomial σ R) = max (max (Cardinal.lift.{u, v} (Cardinal.mk R)) (Cardinal.lift.{v, u} (Cardinal.mk σ))) Cardinal.aleph0

@[simp]

theorem MvPolynomial.cardinal_mk_eq_lift {σ : Type u} {R : Type v} [CommSemiring R] [IsEmpty σ] : Cardinal.mk (MvPolynomial σ R) = Cardinal.lift.{u, v} (Cardinal.mk R)

theorem MvPolynomial.cardinal_lift_mk_le_max {σ : Type u} {R : Type v} [CommSemiring R] : Cardinal.mk (MvPolynomial σ R) ≤ max (max (Cardinal.lift.{u, v} (Cardinal.mk R)) (Cardinal.lift.{v, u} (Cardinal.mk σ))) Cardinal.aleph0

theorem MvPolynomial.cardinal_mk_eq_max {σ : Type u} {R : Type u} [CommSemiring R] [Nonempty σ] [Nontrivial R] : Cardinal.mk (MvPolynomial σ R) = max (max (Cardinal.mk R) (Cardinal.mk σ)) Cardinal.aleph0

theorem MvPolynomial.cardinal_mk_le_max {σ : Type u} {R : Type u} [CommSemiring R] : Cardinal.mk (MvPolynomial σ R) ≤ max (max (Cardinal.mk R) (Cardinal.mk σ)) Cardinal.aleph0

The cardinality of the multivariate polynomial ring, MvPolynomial σ R is at most the maximum of #R, #σ and ℵ₀