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]
:
@[deprecated MvPolynomial.cardinalMk_eq_max_lift (since := "2024-11-10")]
theorem
MvPolynomial.cardinal_mk_eq_max_lift
{σ : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty σ]
[Nontrivial R]
:
Alias of MvPolynomial.cardinalMk_eq_max_lift.
@[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)
@[deprecated MvPolynomial.cardinalMk_eq_lift (since := "2024-11-10")]
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)
Alias of MvPolynomial.cardinalMk_eq_lift.
theorem
MvPolynomial.cardinalMk_eq_one
{σ : Type u}
{R : Type v}
[CommSemiring R]
[Subsingleton R]
:
Cardinal.mk (MvPolynomial σ R) = 1
@[deprecated MvPolynomial.cardinalMk_le_max_lift (since := "2024-11-21")]
Alias of MvPolynomial.cardinalMk_le_max_lift.
theorem
MvPolynomial.cardinalMk_eq_max
{σ R : Type u}
[CommSemiring R]
[Nonempty σ]
[Nontrivial R]
:
Cardinal.mk (MvPolynomial σ R) = Cardinal.mk R ⊔ Cardinal.mk σ ⊔ Cardinal.aleph0
@[deprecated MvPolynomial.cardinalMk_eq_max (since := "2024-11-10")]
theorem
MvPolynomial.cardinal_mk_eq_max
{σ R : Type u}
[CommSemiring R]
[Nonempty σ]
[Nontrivial R]
:
Cardinal.mk (MvPolynomial σ R) = Cardinal.mk R ⊔ Cardinal.mk σ ⊔ Cardinal.aleph0
Alias of MvPolynomial.cardinalMk_eq_max.
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) ≤ Cardinal.mk R ⊔ Cardinal.mk σ ⊔ Cardinal.aleph0
The cardinality of the multivariate polynomial ring, MvPolynomial σ R is at most the maximum
of #R, #σ and ℵ₀
@[deprecated MvPolynomial.cardinalMk_le_max (since := "2024-11-10")]
theorem
MvPolynomial.cardinal_mk_le_max
{σ R : Type u}
[CommSemiring R]
:
Cardinal.mk (MvPolynomial σ R) ≤ Cardinal.mk R ⊔ Cardinal.mk σ ⊔ Cardinal.aleph0
Alias of MvPolynomial.cardinalMk_le_max.
The cardinality of the multivariate polynomial ring, MvPolynomial σ R is at most the maximum
of #R, #σ and ℵ₀