Cardinality of Multivariate Polynomial Ring

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

@[simp]

theorem MvPolynomial.cardinalMk_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.cardinalMk_eq_lift {σ : Type u} {R : Type v} [CommSemiring R] [IsEmpty σ] : Cardinal.mk (MvPolynomial σ R) = Cardinal.lift.{u, v} (Cardinal.mk R)

theorem MvPolynomial.cardinalMk_eq_one {σ : Type u} {R : Type v} [CommSemiring R] [Subsingleton R] : Cardinal.mk (MvPolynomial σ R) = 1

theorem MvPolynomial.cardinalMk_le_max_lift {σ : 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

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

See cardinalMk_le_max for the universe monomorphic version.

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

theorem MvPolynomial.cardinalMk_eq {σ R : Type u} [CommSemiring R] [IsEmpty σ] : Cardinal.mk (MvPolynomial σ R) = Cardinal.mk R

theorem MvPolynomial.cardinalMk_le_max {σ 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 ℵ₀.

See cardinalMk_le_max_lift for the universe polymorphic version.