noncomputable def MvPolynomial.translate {σ : Type u_1} {k : Type u_2} [CommRing k] (p : σ → k) (f : MvPolynomial σ k) : MvPolynomial σ k

Translate a polynomial by p, sending X i to X i + C (p i).

noncomputable def MvPolynomial.minTotalDegree {σ : Type u_1} {k : Type u_2} [CommRing k] (f : MvPolynomial σ k) : ℕ

The minimum total degree among monomials appearing in f (Def 12).

noncomputable def MvPolynomial.multiplicityAt {σ : Type u_1} {k : Type u_2} [CommRing k] (f : MvPolynomial σ k) (p : σ → k) : ℕ

The multiplicity of f at the point p is the minimum total degree of the translated polynomial f(X + p) (Def 12, 13).

@[simp]

theorem MvPolynomial.translate_def {σ : Type u_1} {k : Type u_2} [CommRing k] (p : σ → k) (f : MvPolynomial σ k) : translate p f = (aeval fun (i : σ) => X i + C (p i)) f

Unfolding lemma for translate.

@[simp]

theorem MvPolynomial.minTotalDegree_zero {σ : Type u_1} {k : Type u_2} [CommRing k] : minTotalDegree 0 = 0

The minimum total degree of the zero polynomial is 0 (by convention).

theorem MvPolynomial.minTotalDegree_le_totalDegree {σ : Type u_1} {k : Type u_2} [CommRing k] (f : MvPolynomial σ k) : f.minTotalDegree ≤ f.totalDegree

The minimum total degree is bounded by the (maximum) total degree.

@[simp]

theorem MvPolynomial.translate_zero {σ : Type u_1} {k : Type u_2} [CommRing k] (f : MvPolynomial σ k) : translate 0 f = f

Translating by the zero point is the identity.

noncomputable def MvPolynomial.translateAlgHom {σ : Type u_1} {k : Type u_2} [CommRing k] (p : σ → k) : MvPolynomial σ k →ₐ[k] MvPolynomial σ k

Translation by p packaged as a k-algebra homomorphism.

@[simp]

theorem MvPolynomial.translate_add {σ : Type u_1} {k : Type u_2} [CommRing k] (p : σ → k) (f g : MvPolynomial σ k) : translate p (f + g) = translate p f + translate p g

Translation is additive.

@[simp]

theorem MvPolynomial.translate_mul {σ : Type u_1} {k : Type u_2} [CommRing k] (p : σ → k) (f g : MvPolynomial σ k) : translate p (f * g) = translate p f * translate p g

Translation is multiplicative.