Multivariate polynomials over fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.quotient_mk_comp_C_injective
(σ : Type u)
(K : Type v)
[field K]
(I : ideal (mv_polynomial σ K))
(hI : I ≠ ⊤) :
theorem
mv_polynomial.rank_mv_polynomial
{σ K : Type u}
[field K] :
module.rank K (mv_polynomial σ K) = cardinal.mk (σ →₀ ℕ)