mathlib documentation


Multivariate polynomials over fields #

This file contains basic facts about multivariate polynomials over fields, for example that the dimension of the space of multivariate polynomials over a field is equal to the cardinality of finitely supported functions from the indexing set to .

theorem mv_polynomial.dim_mv_polynomial {σ K : Type u} [field K] :