Documentation

Mathlib.Data.MvPolynomial.Cardinal

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 ℵ₀.

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