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 ⇑((Ideal.Quotient.mk I).comp C)

theorem MvPolynomial.rank_eq_lift {σ : Type u} {K : Type v} [CommRing K] [Nontrivial K] : Module.rank K (MvPolynomial σ K) = Cardinal.lift.{v, u} (Cardinal.mk (σ →₀ ℕ))

theorem MvPolynomial.rank_eq {K : Type v} [CommRing K] [Nontrivial K] {σ : Type v} : Module.rank K (MvPolynomial σ K) = Cardinal.mk (σ →₀ ℕ)

@[instance_reducible]

noncomputable instance MvPolynomial.instModule {σ : Type u} {K : Type v} [CommRing K] : Module K (MvPolynomial σ K)

Equations

• MvPolynomial.instModule = { toDistribMulAction := AddMonoidAlgebra.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }

theorem MvPolynomial.finrank_eq_zero {σ : Type u} {K : Type v} [CommRing K] [Nontrivial K] [Nonempty σ] : Module.finrank K (MvPolynomial σ K) = 0

theorem MvPolynomial.finrank_eq_one {σ : Type u} {K : Type v} [CommRing K] [IsEmpty σ] : Module.finrank K (MvPolynomial σ K) = 1