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