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 MvPolynomial.quotient_mk_comp_C_injective (σ : Type u) (K : Type v) [Field K] (I : Ideal (MvPolynomial σ K)) (hI : I ) :
Function.Injective (( I).comp MvPolynomial.C)