Multivariate polynomials
This file defines polynomial rings over a base ring (or even semiring),
with variables from a general type σ (which could be infinite).
Important definitions
Let R be a commutative ring (or a semiring) and let σ be an arbitrary
type. This file creates the type mv_polynomial σ R, which mathematicians
might denote R[X_i : i ∈ σ]. It is the type of multivariate
(a.k.a. multivariable) polynomials, with variables
corresponding to the terms in σ, and coefficients in R.
Notation
In the definitions below, we use the following notation:
σ : Type*(indexing the variables)R : Type*[comm_semiring R](the coefficients)s : σ →₀ ℕ, a function fromσtoℕwhich is zero away from a finite set. This will give rise to a monomial inmv_polynomial σ Rwhich mathematicians might callX^sa : Ri : σ, with corresponding monomialX i, often denotedX_iby mathematiciansp : mv_polynomial σ R
Definitions
mv_polynomial σ R: the type of polynomials with variables of typeσand coefficients in the commutative semiringRmonomial s a: the monomial which mathematically would be denoteda * X^sC a: the constant polynomial with valueaX i: the degree one monomial corresponding to i; mathematically this might be denotedXᵢ.coeff s p: the coefficient ofsinp.eval₂ (f : R → S) (g : σ → S) p: given a semiring homomorphism fromRto another semiringS, and a mapσ → S, evaluatespat this valuation, returning a term of typeS. Note thateval₂can be made usingevalandmap(see below), and it has been suggested that sticking toevalandmapmight make the code less brittle.eval (g : σ → R) p: given a mapσ → R, evaluatespat this valuation, returning a term of typeRmap (f : R → S) p: returns the multivariate polynomial obtained frompby the change of coefficient semiring corresponding tofdegrees p: the multiset of variables representing the union of the multisets corresponding to each non-zero monomial inp. For example if7 ≠ 0inRandp = x²y+7y³thendegrees p = {x, x, y, y, y}vars p: the finset of variables occurring inp. For example ifp = x⁴y+yzthenvars p = {x, y, z}degree_of n p : ℕ-- the total degree ofpwith respect to the variablen. For example ifp = x⁴y+yzthendegree_of y p = 1.total_degree p : ℕ-- the max of the sizes of the multisetsswhose monomialsX^soccur inp. For example ifp = x⁴y+yzthentotal_degree p = 5.pderivative i p: the partial derivative ofpwith respect toi.
Implementation notes
Recall that if Y has a zero, then X →₀ Y is the type of functions from X to Y with finite
support, i.e. such that only finitely many elements of X get sent to non-zero terms in Y.
The definition of mv_polynomial σ α is (σ →₀ ℕ) →₀ α ; here σ →₀ ℕ denotes the space of all
monomials in the variables, and the function to α sends a monomial to its coefficient in
the polynomial being represented.
Tags
polynomial, multivariate polynomial, multivariable polynomial
Multivariate polynomial, where σ is the index set of the variables and
α is the coefficient ring
Equations
- mv_polynomial σ α = add_monoid_algebra α (σ →₀ ℕ)
@[instance]
def
mv_polynomial.decidable_eq_mv_polynomial
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
[decidable_eq σ]
[decidable_eq α] :
decidable_eq (mv_polynomial σ α)
@[instance]
def
mv_polynomial.comm_semiring
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
comm_semiring (mv_polynomial σ α)
@[instance]
def
mv_polynomial.inhabited
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
inhabited (mv_polynomial σ α)
Equations
- mv_polynomial.inhabited = {default := 0}
@[instance]
def
mv_polynomial.has_scalar
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
has_scalar α (mv_polynomial σ α)
@[instance]
def
mv_polynomial.semimodule
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
semimodule α (mv_polynomial σ α)
@[instance]
def
mv_polynomial.algebra
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
algebra α (mv_polynomial σ α)
Equations
def
mv_polynomial.coeff_coe_to_fun
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
has_coe_to_fun (mv_polynomial σ α)
the coercion turning an mv_polynomial into the function which reports the coefficient of a given monomial
def
mv_polynomial.monomial
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
(σ →₀ ℕ) → α → mv_polynomial σ α
monomial s a is the monomial a * X^s
Equations
- mv_polynomial.monomial s a = finsupp.single s a
C a is the constant polynomial with value a
Equations
- mv_polynomial.C = {to_fun := mv_polynomial.monomial 0, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
theorem
mv_polynomial.algebra_map_eq
(α : Type u)
(σ : Type u_1)
[comm_semiring α] :
algebra_map α (mv_polynomial σ α) = mv_polynomial.C
X n is the degree 1 monomial 1*n
Equations
- mv_polynomial.X n = mv_polynomial.monomial (finsupp.single n 1) 1
@[simp]
@[simp]
theorem
mv_polynomial.C_mul_monomial
{α : Type u}
{σ : Type u_1}
{a a' : α}
{s : σ →₀ ℕ}
[comm_semiring α] :
⇑mv_polynomial.C a * mv_polynomial.monomial s a' = mv_polynomial.monomial s (a * a')
@[simp]
theorem
mv_polynomial.C_add
{α : Type u}
{σ : Type u_1}
{a a' : α}
[comm_semiring α] :
⇑mv_polynomial.C (a + a') = ⇑mv_polynomial.C a + ⇑mv_polynomial.C a'
@[simp]
theorem
mv_polynomial.C_mul
{α : Type u}
{σ : Type u_1}
{a a' : α}
[comm_semiring α] :
⇑mv_polynomial.C (a * a') = ⇑mv_polynomial.C a * ⇑mv_polynomial.C a'
@[simp]
theorem
mv_polynomial.C_pow
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(a : α)
(n : ℕ) :
⇑mv_polynomial.C (a ^ n) = ⇑mv_polynomial.C a ^ n
@[simp]
theorem
mv_polynomial.C_inj
{σ : Type u_1}
(R : Type u_2)
[comm_ring R]
(r s : R) :
⇑mv_polynomial.C r = ⇑mv_polynomial.C s ↔ r = s
theorem
mv_polynomial.C_eq_coe_nat
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(n : ℕ) :
⇑mv_polynomial.C ↑n = ↑n
theorem
mv_polynomial.X_pow_eq_single
{α : Type u}
{σ : Type u_1}
{e : ℕ}
{n : σ}
[comm_semiring α] :
mv_polynomial.X n ^ e = mv_polynomial.monomial (finsupp.single n e) 1
theorem
mv_polynomial.monomial_add_single
{α : Type u}
{σ : Type u_1}
{a : α}
{e : ℕ}
{n : σ}
{s : σ →₀ ℕ}
[comm_semiring α] :
mv_polynomial.monomial (s + finsupp.single n e) a = mv_polynomial.monomial s a * mv_polynomial.X n ^ e
theorem
mv_polynomial.monomial_single_add
{α : Type u}
{σ : Type u_1}
{a : α}
{e : ℕ}
{n : σ}
{s : σ →₀ ℕ}
[comm_semiring α] :
mv_polynomial.monomial (finsupp.single n e + s) a = mv_polynomial.X n ^ e * mv_polynomial.monomial s a
theorem
mv_polynomial.single_eq_C_mul_X
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{s : σ}
{a : α}
{n : ℕ} :
mv_polynomial.monomial (finsupp.single s n) a = ⇑mv_polynomial.C a * mv_polynomial.X s ^ n
@[simp]
theorem
mv_polynomial.monomial_add
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{s : σ →₀ ℕ}
{a b : α} :
mv_polynomial.monomial s a + mv_polynomial.monomial s b = mv_polynomial.monomial s (a + b)
@[simp]
theorem
mv_polynomial.monomial_mul
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{s s' : σ →₀ ℕ}
{a b : α} :
mv_polynomial.monomial s a * mv_polynomial.monomial s' b = mv_polynomial.monomial (s + s') (a * b)
@[simp]
theorem
mv_polynomial.monomial_zero
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{s : σ →₀ ℕ} :
mv_polynomial.monomial s 0 = 0
@[simp]
theorem
mv_polynomial.sum_monomial
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{A : Type u_2}
[add_comm_monoid A]
{u : σ →₀ ℕ}
{r : α}
{b : (σ →₀ ℕ) → α → A} :
b u 0 = 0 → finsupp.sum (mv_polynomial.monomial u r) b = b u r
theorem
mv_polynomial.monomial_eq
{α : Type u}
{σ : Type u_1}
{a : α}
{s : σ →₀ ℕ}
[comm_semiring α] :
mv_polynomial.monomial s a = ⇑mv_polynomial.C a * s.prod (λ (n : σ) (e : ℕ), mv_polynomial.X n ^ e)
theorem
mv_polynomial.induction_on
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{M : mv_polynomial σ α → Prop}
(p : mv_polynomial σ α) :
(∀ (a : α), M (⇑mv_polynomial.C a)) → (∀ (p q : mv_polynomial σ α), M p → M q → M (p + q)) → (∀ (p : mv_polynomial σ α) (n : σ), M p → M (p * mv_polynomial.X n)) → M p
theorem
mv_polynomial.induction_on'
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{P : mv_polynomial σ α → Prop}
(p : mv_polynomial σ α) :
(∀ (u : σ →₀ ℕ) (a : α), P (mv_polynomial.monomial u a)) → (∀ (p q : mv_polynomial σ α), P p → P q → P (p + q)) → P p
theorem
mv_polynomial.hom_eq_hom
{α : Type u}
{γ : Type w}
{σ : Type u_1}
[comm_semiring α]
[semiring γ]
(f g : mv_polynomial σ α →+* γ)
(hC : ∀ (a : α), ⇑f (⇑mv_polynomial.C a) = ⇑g (⇑mv_polynomial.C a))
(hX : ∀ (n : σ), ⇑f (mv_polynomial.X n) = ⇑g (mv_polynomial.X n))
(p : mv_polynomial σ α) :
theorem
mv_polynomial.is_id
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(f : mv_polynomial σ α →+* mv_polynomial σ α)
(hC : ∀ (a : α), ⇑f (⇑mv_polynomial.C a) = ⇑mv_polynomial.C a)
(hX : ∀ (n : σ), ⇑f (mv_polynomial.X n) = mv_polynomial.X n)
(p : mv_polynomial σ α) :
def
mv_polynomial.coeff
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
(σ →₀ ℕ) → mv_polynomial σ α → α
The coefficient of the monomial m in the multi-variable polynomial p.
Equations
- mv_polynomial.coeff m p = ⇑p m
theorem
mv_polynomial.ext
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p q : mv_polynomial σ α) :
(∀ (m : σ →₀ ℕ), mv_polynomial.coeff m p = mv_polynomial.coeff m q) → p = q
theorem
mv_polynomial.ext_iff
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p q : mv_polynomial σ α) :
p = q ↔ ∀ (m : σ →₀ ℕ), mv_polynomial.coeff m p = mv_polynomial.coeff m q
@[simp]
theorem
mv_polynomial.coeff_add
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ)
(p q : mv_polynomial σ α) :
mv_polynomial.coeff m (p + q) = mv_polynomial.coeff m p + mv_polynomial.coeff m q
@[simp]
theorem
mv_polynomial.coeff_zero
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ) :
mv_polynomial.coeff m 0 = 0
@[simp]
theorem
mv_polynomial.coeff_zero_X
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(i : σ) :
mv_polynomial.coeff 0 (mv_polynomial.X i) = 0
@[instance]
def
mv_polynomial.coeff.is_add_monoid_hom
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ) :
Equations
- _ = _
theorem
mv_polynomial.coeff_sum
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{X : Type u_2}
(s : finset X)
(f : X → mv_polynomial σ α)
(m : σ →₀ ℕ) :
mv_polynomial.coeff m (s.sum (λ (x : X), f x)) = s.sum (λ (x : X), mv_polynomial.coeff m (f x))
theorem
mv_polynomial.monic_monomial_eq
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ) :
mv_polynomial.monomial m 1 = m.prod (λ (n : σ) (e : ℕ), mv_polynomial.X n ^ e)
@[simp]
theorem
mv_polynomial.coeff_monomial
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m n : σ →₀ ℕ)
(a : α) :
mv_polynomial.coeff m (mv_polynomial.monomial n a) = ite (n = m) a 0
@[simp]
theorem
mv_polynomial.coeff_C
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ)
(a : α) :
mv_polynomial.coeff m (⇑mv_polynomial.C a) = ite (0 = m) a 0
theorem
mv_polynomial.coeff_X_pow
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(i : σ)
(m : σ →₀ ℕ)
(k : ℕ) :
mv_polynomial.coeff m (mv_polynomial.X i ^ k) = ite (finsupp.single i k = m) 1 0
theorem
mv_polynomial.coeff_X'
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(i : σ)
(m : σ →₀ ℕ) :
mv_polynomial.coeff m (mv_polynomial.X i) = ite (finsupp.single i 1 = m) 1 0
@[simp]
theorem
mv_polynomial.coeff_X
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(i : σ) :
mv_polynomial.coeff (finsupp.single i 1) (mv_polynomial.X i) = 1
@[simp]
theorem
mv_polynomial.coeff_C_mul
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ)
(a : α)
(p : mv_polynomial σ α) :
mv_polynomial.coeff m (⇑mv_polynomial.C a * p) = a * mv_polynomial.coeff m p
theorem
mv_polynomial.coeff_mul
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p q : mv_polynomial σ α)
(n : σ →₀ ℕ) :
mv_polynomial.coeff n (p * q) = n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), mv_polynomial.coeff x.fst p * mv_polynomial.coeff x.snd q)
@[simp]
theorem
mv_polynomial.coeff_mul_X
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ)
(s : σ)
(p : mv_polynomial σ α) :
mv_polynomial.coeff (m + finsupp.single s 1) (p * mv_polynomial.X s) = mv_polynomial.coeff m p
theorem
mv_polynomial.coeff_mul_X'
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(m : σ →₀ ℕ)
(s : σ)
(p : mv_polynomial σ α) :
mv_polynomial.coeff m (p * mv_polynomial.X s) = ite (s ∈ m.support) (mv_polynomial.coeff (m - finsupp.single s 1) p) 0
theorem
mv_polynomial.eq_zero_iff
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{p : mv_polynomial σ α} :
theorem
mv_polynomial.ne_zero_iff
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{p : mv_polynomial σ α} :
theorem
mv_polynomial.exists_coeff_ne_zero
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{p : mv_polynomial σ α} :
p ≠ 0 → (∃ (d : σ →₀ ℕ), mv_polynomial.coeff d p ≠ 0)
@[simp]
theorem
mv_polynomial.support_sum_monomial_coeff
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p : mv_polynomial σ α) :
p.support.sum (λ (v : σ →₀ ℕ), mv_polynomial.monomial v (mv_polynomial.coeff v p)) = p
theorem
mv_polynomial.as_sum
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p : mv_polynomial σ α) :
p = p.support.sum (λ (v : σ →₀ ℕ), mv_polynomial.monomial v (mv_polynomial.coeff v p))
def
mv_polynomial.eval₂
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β] :
(α →+* β) → (σ → β) → mv_polynomial σ α → β
Evaluate a polynomial p given a valuation g of all the variables
and a ring hom f from the scalar ring to the target
Equations
- mv_polynomial.eval₂ f g p = finsupp.sum p (λ (s : σ →₀ ℕ) (a : α), ⇑f a * s.prod (λ (n : σ) (e : ℕ), g n ^ e))
theorem
mv_polynomial.eval₂_eq
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(g : α →+* β)
(x : σ → β)
(f : mv_polynomial σ α) :
theorem
mv_polynomial.eval₂_eq'
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
[fintype σ]
(g : α →+* β)
(x : σ → β)
(f : mv_polynomial σ α) :
mv_polynomial.eval₂ g x f = f.support.sum (λ (d : σ →₀ ℕ), ⇑g (mv_polynomial.coeff d f) * finset.univ.prod (λ (i : σ), x i ^ ⇑d i))
@[simp]
theorem
mv_polynomial.eval₂_zero
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β) :
mv_polynomial.eval₂ f g 0 = 0
@[simp]
theorem
mv_polynomial.eval₂_add
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
{p q : mv_polynomial σ α}
[comm_semiring β]
(f : α →+* β)
(g : σ → β) :
mv_polynomial.eval₂ f g (p + q) = mv_polynomial.eval₂ f g p + mv_polynomial.eval₂ f g q
@[simp]
theorem
mv_polynomial.eval₂_monomial
{α : Type u}
{β : Type v}
{σ : Type u_1}
{a : α}
{s : σ →₀ ℕ}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β) :
mv_polynomial.eval₂ f g (mv_polynomial.monomial s a) = ⇑f a * s.prod (λ (n : σ) (e : ℕ), g n ^ e)
@[simp]
theorem
mv_polynomial.eval₂_C
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
(a : α) :
mv_polynomial.eval₂ f g (⇑mv_polynomial.C a) = ⇑f a
@[simp]
theorem
mv_polynomial.eval₂_one
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β) :
mv_polynomial.eval₂ f g 1 = 1
@[simp]
theorem
mv_polynomial.eval₂_X
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
(n : σ) :
mv_polynomial.eval₂ f g (mv_polynomial.X n) = g n
theorem
mv_polynomial.eval₂_mul_monomial
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
{p : mv_polynomial σ α}
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
{s : σ →₀ ℕ}
{a : α} :
mv_polynomial.eval₂ f g (p * mv_polynomial.monomial s a) = mv_polynomial.eval₂ f g p * ⇑f a * s.prod (λ (n : σ) (e : ℕ), g n ^ e)
@[simp]
theorem
mv_polynomial.eval₂_mul
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
{q : mv_polynomial σ α}
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
{p : mv_polynomial σ α} :
mv_polynomial.eval₂ f g (p * q) = mv_polynomial.eval₂ f g p * mv_polynomial.eval₂ f g q
@[simp]
theorem
mv_polynomial.eval₂_pow
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
{p : mv_polynomial σ α}
{n : ℕ} :
mv_polynomial.eval₂ f g (p ^ n) = mv_polynomial.eval₂ f g p ^ n
@[instance]
def
mv_polynomial.eval₂.is_semiring_hom
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β) :
Equations
- _ = _
def
mv_polynomial.eval₂_hom
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β] :
(α →+* β) → (σ → β) → mv_polynomial σ α →+* β
mv_polynomial.eval₂ as a ring_hom.
Equations
@[simp]
theorem
mv_polynomial.coe_eval₂_hom
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β) :
⇑(mv_polynomial.eval₂_hom f g) = mv_polynomial.eval₂ f g
theorem
mv_polynomial.eval₂_hom_congr
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
{f₁ f₂ : α →+* β}
{g₁ g₂ : σ → β}
{p₁ p₂ : mv_polynomial σ α} :
f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → ⇑(mv_polynomial.eval₂_hom f₁ g₁) p₁ = ⇑(mv_polynomial.eval₂_hom f₂ g₂) p₂
theorem
mv_polynomial.eval₂_comp_left
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
{γ : Type u_2}
[comm_semiring γ]
(k : β →+* γ)
(f : α →+* β)
(g : σ → β)
(p : mv_polynomial σ α) :
⇑k (mv_polynomial.eval₂ f g p) = mv_polynomial.eval₂ (k.comp f) (⇑k ∘ g) p
@[simp]
theorem
mv_polynomial.eval₂_eta
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p : mv_polynomial σ α) :
theorem
mv_polynomial.eval₂_congr
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
{p : mv_polynomial σ α}
[comm_semiring β]
(f : α →+* β)
(g₁ g₂ : σ → β) :
(∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → mv_polynomial.coeff c p ≠ 0 → g₁ i = g₂ i) → mv_polynomial.eval₂ f g₁ p = mv_polynomial.eval₂ f g₂ p
@[simp]
theorem
mv_polynomial.eval₂_prod
{α : Type u}
{β : Type v}
{γ : Type w}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
(s : finset γ)
(p : γ → mv_polynomial σ α) :
mv_polynomial.eval₂ f g (s.prod (λ (x : γ), p x)) = s.prod (λ (x : γ), mv_polynomial.eval₂ f g (p x))
@[simp]
theorem
mv_polynomial.eval₂_sum
{α : Type u}
{β : Type v}
{γ : Type w}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
(s : finset γ)
(p : γ → mv_polynomial σ α) :
mv_polynomial.eval₂ f g (s.sum (λ (x : γ), p x)) = s.sum (λ (x : γ), mv_polynomial.eval₂ f g (p x))
theorem
mv_polynomial.eval₂_assoc
{α : Type u}
{β : Type v}
{γ : Type w}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
(q : γ → mv_polynomial σ α)
(p : mv_polynomial γ α) :
mv_polynomial.eval₂ f (λ (t : γ), mv_polynomial.eval₂ f g (q t)) p = mv_polynomial.eval₂ f g (mv_polynomial.eval₂ mv_polynomial.C q p)
def
mv_polynomial.eval
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
(σ → α) → mv_polynomial σ α →+* α
Evaluate a polynomial p given a valuation f of all the variables
Equations
theorem
mv_polynomial.eval_eq
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(x : σ → α)
(f : mv_polynomial σ α) :
theorem
mv_polynomial.eval_eq'
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
[fintype σ]
(x : σ → α)
(f : mv_polynomial σ α) :
⇑(mv_polynomial.eval x) f = f.support.sum (λ (d : σ →₀ ℕ), mv_polynomial.coeff d f * finset.univ.prod (λ (i : σ), x i ^ ⇑d i))
theorem
mv_polynomial.eval_monomial
{α : Type u}
{σ : Type u_1}
{a : α}
{s : σ →₀ ℕ}
[comm_semiring α]
{f : σ → α} :
⇑(mv_polynomial.eval f) (mv_polynomial.monomial s a) = a * s.prod (λ (n : σ) (e : ℕ), f n ^ e)
@[simp]
theorem
mv_polynomial.eval_C
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{f : σ → α}
(a : α) :
⇑(mv_polynomial.eval f) (⇑mv_polynomial.C a) = a
@[simp]
theorem
mv_polynomial.eval_X
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{f : σ → α}
(n : σ) :
⇑(mv_polynomial.eval f) (mv_polynomial.X n) = f n
theorem
mv_polynomial.eval_sum
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{ι : Type u_2}
(s : finset ι)
(f : ι → mv_polynomial σ α)
(g : σ → α) :
⇑(mv_polynomial.eval g) (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ⇑(mv_polynomial.eval g) (f i))
theorem
mv_polynomial.eval_prod
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{ι : Type u_2}
(s : finset ι)
(f : ι → mv_polynomial σ α)
(g : σ → α) :
⇑(mv_polynomial.eval g) (s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), ⇑(mv_polynomial.eval g) (f i))
theorem
mv_polynomial.eval_assoc
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{τ : Type u_2}
(f : σ → mv_polynomial τ α)
(g : τ → α)
(p : mv_polynomial σ α) :
⇑(mv_polynomial.eval (⇑(mv_polynomial.eval g) ∘ f)) p = ⇑(mv_polynomial.eval g) (mv_polynomial.eval₂ mv_polynomial.C f p)
def
mv_polynomial.map
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β] :
(α →+* β) → mv_polynomial σ α →+* mv_polynomial σ β
map f p maps a polynomial p across a ring hom f
Equations
@[simp]
theorem
mv_polynomial.map_monomial
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(s : σ →₀ ℕ)
(a : α) :
⇑(mv_polynomial.map f) (mv_polynomial.monomial s a) = mv_polynomial.monomial s (⇑f a)
@[simp]
theorem
mv_polynomial.map_C
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(a : α) :
⇑(mv_polynomial.map f) (⇑mv_polynomial.C a) = ⇑mv_polynomial.C (⇑f a)
@[simp]
theorem
mv_polynomial.map_X
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(n : σ) :
⇑(mv_polynomial.map f) (mv_polynomial.X n) = mv_polynomial.X n
theorem
mv_polynomial.map_id
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p : mv_polynomial σ α) :
⇑(mv_polynomial.map (ring_hom.id α)) p = p
theorem
mv_polynomial.map_map
{α : Type u}
{β : Type v}
{γ : Type w}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
[comm_semiring γ]
(g : β →+* γ)
(p : mv_polynomial σ α) :
⇑(mv_polynomial.map g) (⇑(mv_polynomial.map f) p) = ⇑(mv_polynomial.map (g.comp f)) p
theorem
mv_polynomial.eval₂_eq_eval_map
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : σ → β)
(p : mv_polynomial σ α) :
mv_polynomial.eval₂ f g p = ⇑(mv_polynomial.eval g) (⇑(mv_polynomial.map f) p)
theorem
mv_polynomial.eval₂_comp_right
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
{γ : Type u_2}
[comm_semiring γ]
(k : β →+* γ)
(f : α →+* β)
(g : σ → β)
(p : mv_polynomial σ α) :
⇑k (mv_polynomial.eval₂ f g p) = mv_polynomial.eval₂ k (⇑k ∘ g) (⇑(mv_polynomial.map f) p)
theorem
mv_polynomial.map_eval₂
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : γ → mv_polynomial δ α)
(p : mv_polynomial γ α) :
⇑(mv_polynomial.map f) (mv_polynomial.eval₂ mv_polynomial.C g p) = mv_polynomial.eval₂ mv_polynomial.C (⇑(mv_polynomial.map f) ∘ g) (⇑(mv_polynomial.map f) p)
theorem
mv_polynomial.coeff_map
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(p : mv_polynomial σ α)
(m : σ →₀ ℕ) :
mv_polynomial.coeff m (⇑(mv_polynomial.map f) p) = ⇑f (mv_polynomial.coeff m p)
theorem
mv_polynomial.map_injective
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β) :
def
mv_polynomial.degrees
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
mv_polynomial σ α → multiset σ
The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.
(For example, degrees (x^2 * y + y^3) would be {x, x, y, y, y}.)
theorem
mv_polynomial.degrees_monomial
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(s : σ →₀ ℕ)
(a : α) :
(mv_polynomial.monomial s a).degrees ≤ s.to_multiset
theorem
mv_polynomial.degrees_monomial_eq
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(s : σ →₀ ℕ)
(a : α) :
a ≠ 0 → (mv_polynomial.monomial s a).degrees = s.to_multiset
theorem
mv_polynomial.degrees_C
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(a : α) :
(⇑mv_polynomial.C a).degrees = 0
theorem
mv_polynomial.degrees_X
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(n : σ) :
(mv_polynomial.X n).degrees ≤ {n}
theorem
mv_polynomial.degrees_add
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p q : mv_polynomial σ α) :
theorem
mv_polynomial.degrees_sum
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{ι : Type u_2}
(s : finset ι)
(f : ι → mv_polynomial σ α) :
theorem
mv_polynomial.degrees_mul
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p q : mv_polynomial σ α) :
theorem
mv_polynomial.degrees_prod
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{ι : Type u_2}
(s : finset ι)
(f : ι → mv_polynomial σ α) :
theorem
mv_polynomial.degrees_pow
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p : mv_polynomial σ α)
(n : ℕ) :
def
mv_polynomial.vars
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
mv_polynomial σ α → finset σ
vars p is the set of variables appearing in the polynomial p
@[simp]
@[simp]
theorem
mv_polynomial.vars_monomial
{α : Type u}
{σ : Type u_1}
{a : α}
{s : σ →₀ ℕ}
[comm_semiring α] :
a ≠ 0 → (mv_polynomial.monomial s a).vars = s.support
@[simp]
theorem
mv_polynomial.vars_C
{α : Type u}
{σ : Type u_1}
{a : α}
[comm_semiring α] :
(⇑mv_polynomial.C a).vars = ∅
@[simp]
theorem
mv_polynomial.vars_X
{α : Type u}
{σ : Type u_1}
{n : σ}
[comm_semiring α] :
0 ≠ 1 → (mv_polynomial.X n).vars = {n}
theorem
mv_polynomial.mem_support_not_mem_vars_zero
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{f : mv_polynomial σ α}
{x : σ →₀ ℕ}
(H : x ∈ f.support)
{v : σ} :
def
mv_polynomial.degree_of
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
σ → mv_polynomial σ α → ℕ
degree_of n p gives the highest power of X_n that appears in p
Equations
def
mv_polynomial.total_degree
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
mv_polynomial σ α → ℕ
total_degree p gives the maximum |s| over the monomials X^s in p
theorem
mv_polynomial.total_degree_eq
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p : mv_polynomial σ α) :
p.total_degree = p.support.sup (λ (m : σ →₀ ℕ), m.to_multiset.card)
theorem
mv_polynomial.total_degree_le_degrees_card
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(p : mv_polynomial σ α) :
p.total_degree ≤ p.degrees.card
@[simp]
theorem
mv_polynomial.total_degree_C
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(a : α) :
(⇑mv_polynomial.C a).total_degree = 0
@[simp]
theorem
mv_polynomial.total_degree_zero
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
0.total_degree = 0
@[simp]
theorem
mv_polynomial.total_degree_one
{α : Type u}
{σ : Type u_1}
[comm_semiring α] :
1.total_degree = 0
@[simp]
theorem
mv_polynomial.total_degree_X
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
[nontrivial α]
(s : σ) :
(mv_polynomial.X s).total_degree = 1
theorem
mv_polynomial.total_degree_add
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(a b : mv_polynomial σ α) :
(a + b).total_degree ≤ max a.total_degree b.total_degree
theorem
mv_polynomial.total_degree_mul
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(a b : mv_polynomial σ α) :
(a * b).total_degree ≤ a.total_degree + b.total_degree
theorem
mv_polynomial.total_degree_pow
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(a : mv_polynomial σ α)
(n : ℕ) :
(a ^ n).total_degree ≤ n * a.total_degree
theorem
mv_polynomial.total_degree_list_prod
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(s : list (mv_polynomial σ α)) :
theorem
mv_polynomial.total_degree_multiset_prod
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
(s : multiset (mv_polynomial σ α)) :
theorem
mv_polynomial.total_degree_finset_prod
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{ι : Type u_2}
(s : finset ι)
(f : ι → mv_polynomial σ α) :
(s.prod f).total_degree ≤ s.sum (λ (i : ι), (f i).total_degree)
theorem
mv_polynomial.exists_degree_lt
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
[fintype σ]
(f : mv_polynomial σ α)
(n : ℕ)
(h : f.total_degree < n * fintype.card σ)
{d : σ →₀ ℕ} :
theorem
mv_polynomial.coeff_eq_zero_of_total_degree_lt
{α : Type u}
{σ : Type u_1}
[comm_semiring α]
{f : mv_polynomial σ α}
{d : σ →₀ ℕ} :
f.total_degree < d.support.sum (λ (i : σ), ⇑d i) → mv_polynomial.coeff d f = 0
The algebra of multivariate polynomials
def
mv_polynomial.aeval
{σ : Type u_1}
{R : Type u}
{A : Type v}
(f : σ → A)
[comm_semiring R]
[comm_semiring A]
[algebra R A] :
mv_polynomial σ R →ₐ[R] A
A map σ → A where A is an algebra over R generates an R-algebra homomorphism
from multivariate polynomials over σ to A.
Equations
- mv_polynomial.aeval f = {to_fun := (mv_polynomial.eval₂_hom (algebra_map R A) f).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
mv_polynomial.aeval_def
{σ : Type u_1}
{R : Type u}
{A : Type v}
(f : σ → A)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(p : mv_polynomial σ R) :
⇑(mv_polynomial.aeval f) p = mv_polynomial.eval₂ (algebra_map R A) f p
@[simp]
theorem
mv_polynomial.aeval_X
{σ : Type u_1}
{R : Type u}
{A : Type v}
(f : σ → A)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s : σ) :
⇑(mv_polynomial.aeval f) (mv_polynomial.X s) = f s
@[simp]
theorem
mv_polynomial.aeval_C
{σ : Type u_1}
{R : Type u}
{A : Type v}
(f : σ → A)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(r : R) :
⇑(mv_polynomial.aeval f) (⇑mv_polynomial.C r) = ⇑(algebra_map R A) r
theorem
mv_polynomial.eval_unique
{σ : Type u_1}
{R : Type u}
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(φ : mv_polynomial σ R →ₐ[R] A) :
@[instance]
def
mv_polynomial.comm_ring
{α : Type u}
{σ : Type u_1}
[comm_ring α] :
comm_ring (mv_polynomial σ α)
@[simp]
theorem
mv_polynomial.C_sub
{α : Type u}
(σ : Type u_1)
(a a' : α)
[comm_ring α] :
⇑mv_polynomial.C (a - a') = ⇑mv_polynomial.C a - ⇑mv_polynomial.C a'
@[simp]
@[simp]
theorem
mv_polynomial.coeff_neg
{α : Type u}
(σ : Type u_1)
[comm_ring α]
(m : σ →₀ ℕ)
(p : mv_polynomial σ α) :
mv_polynomial.coeff m (-p) = -mv_polynomial.coeff m p
@[simp]
theorem
mv_polynomial.coeff_sub
{α : Type u}
(σ : Type u_1)
[comm_ring α]
(m : σ →₀ ℕ)
(p q : mv_polynomial σ α) :
mv_polynomial.coeff m (p - q) = mv_polynomial.coeff m p - mv_polynomial.coeff m q
@[instance]
Equations
theorem
mv_polynomial.C_mul'
{α : Type u}
{σ : Type u_1}
(a : α)
[comm_ring α]
(p : mv_polynomial σ α) :
⇑mv_polynomial.C a * p = a • p
theorem
mv_polynomial.smul_eq_C_mul
{α : Type u}
{σ : Type u_1}
[comm_ring α]
(p : mv_polynomial σ α)
(a : α) :
a • p = ⇑mv_polynomial.C a * p
@[simp]
theorem
mv_polynomial.smul_eval
{α : Type u}
{σ : Type u_1}
[comm_ring α]
(x : σ → α)
(p : mv_polynomial σ α)
(s : α) :
⇑(mv_polynomial.eval x) (s • p) = s * ⇑(mv_polynomial.eval x) p
theorem
mv_polynomial.degrees_neg
{α : Type u}
{σ : Type u_1}
[comm_ring α]
(p : mv_polynomial σ α) :
theorem
mv_polynomial.degrees_sub
{α : Type u}
{σ : Type u_1}
[comm_ring α]
(p q : mv_polynomial σ α) :
@[simp]
theorem
mv_polynomial.eval₂_sub
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_ring α]
(p : mv_polynomial σ α)
{q : mv_polynomial σ α}
[comm_ring β]
(f : α →+* β)
(g : σ → β) :
mv_polynomial.eval₂ f g (p - q) = mv_polynomial.eval₂ f g p - mv_polynomial.eval₂ f g q
@[simp]
theorem
mv_polynomial.eval₂_neg
{α : Type u}
{β : Type v}
{σ : Type u_1}
[comm_ring α]
(p : mv_polynomial σ α)
[comm_ring β]
(f : α →+* β)
(g : σ → β) :
mv_polynomial.eval₂ f g (-p) = -mv_polynomial.eval₂ f g p
theorem
mv_polynomial.hom_C
{β : Type v}
{σ : Type u_1}
[comm_ring β]
(f : mv_polynomial σ ℤ → β)
[is_ring_hom f]
(n : ℤ) :
f (⇑mv_polynomial.C n) = ↑n
@[simp]
theorem
mv_polynomial.eval₂_hom_X
{β : Type v}
[comm_ring β]
{α : Type u}
(c : ℤ →+* β)
(f : mv_polynomial α ℤ →+* β)
(x : mv_polynomial α ℤ) :
mv_polynomial.eval₂ c (⇑f ∘ mv_polynomial.X) x = ⇑f x
A ring homomorphism f : Z[X_1, X_2, ...] → R is determined by the evaluations f(X_1), f(X_2), ...
def
mv_polynomial.hom_equiv
{β : Type v}
{σ : Type u_1}
[comm_ring β] :
(mv_polynomial σ ℤ →+* β) ≃ (σ → β)
Ring homomorphisms out of integer polynomials on a type σ are the same as
functions out of the type σ,
Equations
- mv_polynomial.hom_equiv = {to_fun := λ (f : mv_polynomial σ ℤ →+* β), ⇑f ∘ mv_polynomial.X, inv_fun := λ (f : σ → β), mv_polynomial.eval₂_hom (int.cast_ring_hom β) f, left_inv := _, right_inv := _}
@[simp]
theorem
mv_polynomial.total_degree_neg
{α : Type u}
{σ : Type u_1}
[comm_ring α]
(a : mv_polynomial σ α) :
(-a).total_degree = a.total_degree
theorem
mv_polynomial.total_degree_sub
{α : Type u}
{σ : Type u_1}
[comm_ring α]
(a b : mv_polynomial σ α) :
(a - b).total_degree ≤ max a.total_degree b.total_degree
def
mv_polynomial.rename
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring α] :
(β → γ) → mv_polynomial β α →+* mv_polynomial γ α
Rename all the variables in a multivariable polynomial.
Equations
@[simp]
theorem
mv_polynomial.rename_C
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring α]
(f : β → γ)
(a : α) :
@[simp]
theorem
mv_polynomial.rename_X
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring α]
(f : β → γ)
(b : β) :
⇑(mv_polynomial.rename f) (mv_polynomial.X b) = mv_polynomial.X (f b)
theorem
mv_polynomial.map_rename
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(g : γ → δ)
(p : mv_polynomial γ α) :
⇑(mv_polynomial.map f) (⇑(mv_polynomial.rename g) p) = ⇑(mv_polynomial.rename g) (⇑(mv_polynomial.map f) p)
@[simp]
theorem
mv_polynomial.rename_rename
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
(f : β → γ)
(g : γ → δ)
(p : mv_polynomial β α) :
⇑(mv_polynomial.rename g) (⇑(mv_polynomial.rename f) p) = ⇑(mv_polynomial.rename (g ∘ f)) p
@[simp]
theorem
mv_polynomial.rename_id
{α : Type u}
{β : Type v}
[comm_semiring α]
(p : mv_polynomial β α) :
⇑(mv_polynomial.rename id) p = p
theorem
mv_polynomial.rename_monomial
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring α]
(f : β → γ)
(p : β →₀ ℕ)
(a : α) :
⇑(mv_polynomial.rename f) (mv_polynomial.monomial p a) = mv_polynomial.monomial (finsupp.map_domain f p) a
theorem
mv_polynomial.rename_eq
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring α]
(f : β → γ)
(p : mv_polynomial β α) :
⇑(mv_polynomial.rename f) p = finsupp.map_domain (finsupp.map_domain f) p
theorem
mv_polynomial.rename_injective
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring α]
(f : β → γ) :
theorem
mv_polynomial.total_degree_rename_le
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring α]
(f : β → γ)
(p : mv_polynomial β α) :
(⇑(mv_polynomial.rename f) p).total_degree ≤ p.total_degree
theorem
mv_polynomial.eval₂_rename
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(k : γ → δ)
(g : δ → β)
(p : mv_polynomial γ α) :
mv_polynomial.eval₂ f g (⇑(mv_polynomial.rename k) p) = mv_polynomial.eval₂ f (g ∘ k) p
theorem
mv_polynomial.rename_eval₂
{α : Type u}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
(k : γ → δ)
(p : mv_polynomial γ α)
(g : δ → mv_polynomial γ α) :
⇑(mv_polynomial.rename k) (mv_polynomial.eval₂ mv_polynomial.C (g ∘ k) p) = mv_polynomial.eval₂ mv_polynomial.C (⇑(mv_polynomial.rename k) ∘ g) (⇑(mv_polynomial.rename k) p)
theorem
mv_polynomial.rename_prodmk_eval₂
{α : Type u}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
(p : mv_polynomial γ α)
(d : δ)
(g : γ → mv_polynomial γ α) :
⇑(mv_polynomial.rename (prod.mk d)) (mv_polynomial.eval₂ mv_polynomial.C g p) = mv_polynomial.eval₂ mv_polynomial.C (λ (x : γ), ⇑(mv_polynomial.rename (prod.mk d)) (g x)) p
theorem
mv_polynomial.eval₂_rename_prodmk
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
[comm_semiring β]
(f : α →+* β)
(p : mv_polynomial γ α)
(g : δ × γ → β)
(d : δ) :
mv_polynomial.eval₂ f g (⇑(mv_polynomial.rename (prod.mk d)) p) = mv_polynomial.eval₂ f (λ (i : γ), g (d, i)) p
theorem
mv_polynomial.eval_rename_prodmk
{α : Type u}
{γ : Type w}
{δ : Type x}
[comm_semiring α]
(p : mv_polynomial γ α)
(g : δ × γ → α)
(d : δ) :
⇑(mv_polynomial.eval g) (⇑(mv_polynomial.rename (prod.mk d)) p) = ⇑(mv_polynomial.eval (λ (i : γ), g (d, i))) p
theorem
mv_polynomial.exists_finset_rename
{α : Type u}
{γ : Type w}
[comm_semiring α]
(p : mv_polynomial γ α) :
∃ (s : finset γ) (q : mv_polynomial {x // x ∈ s} α), p = ⇑(mv_polynomial.rename coe) q
Every polynomial is a polynomial in finitely many variables.
theorem
mv_polynomial.exists_fin_rename
{α : Type u}
{γ : Type w}
[comm_semiring α]
(p : mv_polynomial γ α) :
∃ (n : ℕ) (f : fin n → γ) (hf : function.injective f) (q : mv_polynomial (fin n) α), p = ⇑(mv_polynomial.rename f) q
Every polynomial is a polynomial in finitely many variables.
theorem
mv_polynomial.eval₂_cast_comp
{β : Type u}
{γ : Type v}
(f : γ → β)
{α : Type w}
[comm_ring α]
(c : ℤ →+* α)
(g : β → α)
(x : mv_polynomial γ ℤ) :
mv_polynomial.eval₂ c (g ∘ f) x = mv_polynomial.eval₂ c g (⇑(mv_polynomial.rename f) x)
The ring isomorphism between multivariable polynomials in no variables and the ground ring.
Equations
- mv_polynomial.pempty_ring_equiv α = {to_fun := mv_polynomial.eval₂ (ring_hom.id α) pempty.elim, inv_fun := ⇑mv_polynomial.C, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
The ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.
Equations
- mv_polynomial.punit_ring_equiv α = {to_fun := mv_polynomial.eval₂ polynomial.C (λ (u : punit), polynomial.X), inv_fun := polynomial.eval₂ mv_polynomial.C (mv_polynomial.X punit.star), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
def
mv_polynomial.ring_equiv_of_equiv
(α : Type u)
{β : Type v}
{γ : Type w}
[comm_semiring α] :
β ≃ γ → mv_polynomial β α ≃+* mv_polynomial γ α
The ring isomorphism between multivariable polynomials induced by an equivalence of the variables.
def
mv_polynomial.ring_equiv_congr
(α : Type u)
{β : Type v}
{γ : Type w}
[comm_semiring α]
[comm_semiring γ] :
α ≃+* γ → mv_polynomial β α ≃+* mv_polynomial β γ
The ring isomorphism between multivariable polynomials induced by a ring isomorphism of the ground ring.
def
mv_polynomial.sum_to_iter
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α] :
mv_polynomial (β ⊕ γ) α →+* mv_polynomial β (mv_polynomial γ α)
The function from multivariable polynomials in a sum of two types, to multivariable polynomials in one of the types, with coefficents in multivariable polynomials in the other type.
See sum_ring_equiv for the ring isomorphism.
Equations
- mv_polynomial.sum_to_iter α β γ = mv_polynomial.eval₂_hom (mv_polynomial.C.comp mv_polynomial.C) (λ (bc : β ⊕ γ), bc.rec_on mv_polynomial.X (⇑mv_polynomial.C ∘ mv_polynomial.X))
@[instance]
def
mv_polynomial.is_semiring_hom_sum_to_iter
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α] :
Equations
- _ = _
theorem
mv_polynomial.sum_to_iter_C
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α]
(a : α) :
⇑(mv_polynomial.sum_to_iter α β γ) (⇑mv_polynomial.C a) = ⇑mv_polynomial.C (⇑mv_polynomial.C a)
theorem
mv_polynomial.sum_to_iter_Xl
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α]
(b : β) :
⇑(mv_polynomial.sum_to_iter α β γ) (mv_polynomial.X (sum.inl b)) = mv_polynomial.X b
theorem
mv_polynomial.sum_to_iter_Xr
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α]
(c : γ) :
⇑(mv_polynomial.sum_to_iter α β γ) (mv_polynomial.X (sum.inr c)) = ⇑mv_polynomial.C (mv_polynomial.X c)
def
mv_polynomial.iter_to_sum
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α] :
mv_polynomial β (mv_polynomial γ α) →+* mv_polynomial (β ⊕ γ) α
The function from multivariable polynomials in one type, with coefficents in multivariable polynomials in another type, to multivariable polynomials in the sum of the two types.
See sum_ring_equiv for the ring isomorphism.
Equations
theorem
mv_polynomial.iter_to_sum_C_C
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α]
(a : α) :
⇑(mv_polynomial.iter_to_sum α β γ) (⇑mv_polynomial.C (⇑mv_polynomial.C a)) = ⇑mv_polynomial.C a
theorem
mv_polynomial.iter_to_sum_X
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α]
(b : β) :
⇑(mv_polynomial.iter_to_sum α β γ) (mv_polynomial.X b) = mv_polynomial.X (sum.inl b)
theorem
mv_polynomial.iter_to_sum_C_X
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α]
(c : γ) :
⇑(mv_polynomial.iter_to_sum α β γ) (⇑mv_polynomial.C (mv_polynomial.X c)) = mv_polynomial.X (sum.inr c)
def
mv_polynomial.mv_polynomial_equiv_mv_polynomial
(α : Type u)
(β : Type v)
(γ : Type w)
(δ : Type x)
[comm_semiring α]
[comm_semiring δ]
(f : mv_polynomial β α →+* mv_polynomial γ δ)
(g : mv_polynomial γ δ →+* mv_polynomial β α) :
(∀ (a : δ), ⇑f (⇑g (⇑mv_polynomial.C a)) = ⇑mv_polynomial.C a) → (∀ (n : γ), ⇑f (⇑g (mv_polynomial.X n)) = mv_polynomial.X n) → (∀ (a : α), ⇑g (⇑f (⇑mv_polynomial.C a)) = ⇑mv_polynomial.C a) → (∀ (n : β), ⇑g (⇑f (mv_polynomial.X n)) = mv_polynomial.X n) → mv_polynomial β α ≃+* mv_polynomial γ δ
A helper function for sum_ring_equiv.
def
mv_polynomial.sum_ring_equiv
(α : Type u)
(β : Type v)
(γ : Type w)
[comm_semiring α] :
mv_polynomial (β ⊕ γ) α ≃+* mv_polynomial β (mv_polynomial γ α)
The ring isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficents in multivariable polynomials in the other type.
Equations
- mv_polynomial.sum_ring_equiv α β γ = mv_polynomial.mv_polynomial_equiv_mv_polynomial α (β ⊕ γ) β (mv_polynomial γ α) (mv_polynomial.sum_to_iter α β γ) (mv_polynomial.iter_to_sum α β γ) _ _ _ _
def
mv_polynomial.option_equiv_left
(α : Type u)
(β : Type v)
[comm_semiring α] :
mv_polynomial (option β) α ≃+* polynomial (mv_polynomial β α)
The ring isomorphism between multivariable polynomials in option β and
polynomials with coefficients in mv_polynomial β α.
Equations
def
mv_polynomial.option_equiv_right
(α : Type u)
(β : Type v)
[comm_semiring α] :
mv_polynomial (option β) α ≃+* mv_polynomial β (polynomial α)
The ring isomorphism between multivariable polynomials in option β and
multivariable polynomials with coefficients in polynomials.
def
mv_polynomial.fin_succ_equiv
(α : Type u)
[comm_semiring α]
(n : ℕ) :
mv_polynomial (fin (n + 1)) α ≃+* polynomial (mv_polynomial (fin n) α)
The ring isomorphism between multivariable polynomials in fin (n + 1) and
polynomials over multivariable polynomials in fin n.
Equations
Partial derivatives
def
mv_polynomial.pderivative
{R : Type}
[comm_ring R]
{S : Type} :
S → mv_polynomial S R → mv_polynomial S R
pderivative v p is the partial derivative of p with respect to v
Equations
- mv_polynomial.pderivative v p = finsupp.sum p (λ (A : S →₀ ℕ) (B : R), mv_polynomial.monomial (A - finsupp.single v 1) (B * ↑(⇑A v)))
@[simp]
theorem
mv_polynomial.pderivative_add
{R : Type}
[comm_ring R]
{S : Type}
{v : S}
{f g : mv_polynomial S R} :
mv_polynomial.pderivative v (f + g) = mv_polynomial.pderivative v f + mv_polynomial.pderivative v g
@[simp]
theorem
mv_polynomial.pderivative_monomial
{R : Type}
[comm_ring R]
{S : Type}
{v : S}
{u : S →₀ ℕ}
{a : R} :
mv_polynomial.pderivative v (mv_polynomial.monomial u a) = mv_polynomial.monomial (u - finsupp.single v 1) (a * ↑(⇑u v))
@[simp]
@[simp]
theorem
mv_polynomial.pderivative_zero
{R : Type}
[comm_ring R]
{S : Type}
{v : S} :
mv_polynomial.pderivative v 0 = 0
def
mv_polynomial.pderivative.add_monoid_hom
(R : Type)
[comm_ring R]
{S : Type} :
S → mv_polynomial S R →+ mv_polynomial S R
pderivative : S → mv_polynomial S R → mv_polynomial S R as an add_monoid_hom
Equations
- mv_polynomial.pderivative.add_monoid_hom R v = {to_fun := mv_polynomial.pderivative v, map_zero' := _, map_add' := _}
@[simp]
theorem
mv_polynomial.pderivative.add_monoid_hom_apply
(R : Type)
[comm_ring R]
{S : Type}
(v : S)
(p : mv_polynomial S R) :
theorem
mv_polynomial.pderivative_eq_zero_of_not_mem_vars
{R : Type}
[comm_ring R]
{S : Type}
{v : S}
{f : mv_polynomial S R} :
v ∉ f.vars → mv_polynomial.pderivative v f = 0
theorem
mv_polynomial.pderivative_monomial_single
{R : Type}
[comm_ring R]
{S : Type}
{a : R}
{v : S}
{n : ℕ} :
mv_polynomial.pderivative v (mv_polynomial.monomial (finsupp.single v n) a) = mv_polynomial.monomial (finsupp.single v (n - 1)) (a * ↑n)
theorem
mv_polynomial.pderivative_monomial_mul
{R : Type}
[comm_ring R]
{S : Type}
{v : S}
{u u' : S →₀ ℕ}
{r r' : R} :
mv_polynomial.pderivative v (mv_polynomial.monomial u r * mv_polynomial.monomial u' r') = mv_polynomial.pderivative v (mv_polynomial.monomial u r) * mv_polynomial.monomial u' r' + mv_polynomial.monomial u r * mv_polynomial.pderivative v (mv_polynomial.monomial u' r')
@[simp]
theorem
mv_polynomial.pderivative_mul
{R : Type}
[comm_ring R]
{S : Type}
{v : S}
{f g : mv_polynomial S R} :
mv_polynomial.pderivative v (f * g) = mv_polynomial.pderivative v f * g + f * mv_polynomial.pderivative v g
@[simp]
theorem
mv_polynomial.pderivative_C_mul
{R : Type}
[comm_ring R]
{S : Type}
{a : R}
{f : mv_polynomial S R}
{v : S} :