mathlib documentation

data.mv_polynomial.cardinal

Cardinality of Polynomial Ring #

The main result in this file is mv_polynomial.cardinal_mk_le_max, which says that the cardinality of mv_polynomial σ R is bounded above by the maximum of #R, #σ and ω.

source
theorem mv_polynomial.cardinal_mk_le_max {σ R : Type u} [comm_semiring R] :
# (mv_polynomial σ R) ≤ max (max (# R) (# σ)) ω

The cardinality of the multivariate polynomial ring, mv_polynomial σ R is at most the maximum of #R, #σ and ω