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_one {σ : Type u} {R : Type v} [CommSemiring R] [Subsingleton R] :
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] :
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.