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 (σ →₀ ℕ)
@[implicit_reducible]
noncomputable instance
MvPolynomial.instModule
{σ : Type u}
{K : Type v}
[CommRing K]
:
Module K (MvPolynomial σ K)
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