Polynomial rings

• \(K\[X\]\) is a Euclidean ring when \(K\) is a field
• Irreducible polynomial

DefinitionCyclotomic polynomials in \(\Q[X]\)#

The n-th cyclotomic polynomial with coefficients in R.

Polynomial.cyclotomic.{u_1} (n : ℕ) (R : Type u_1) [Ring R] : Polynomial R

Sources

• Mathlib documentation: Polynomial.cyclotomic
• Source of Polynomial.cyclotomic in Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
• Mathlib undergraduate list: Ring Theory › Polynomial rings

MathlibPolynomial.cyclotomic

Uses 2 · Used by 1

Statement usesField \(\C\) of complex numbers · Roots of a polynomial

Used byThe Solution of a Cubic

• Eisenstein's criterion
• Polynomial algebra in one or several indeterminates over a commutative ring
• Roots of a polynomial
• Multiplicity

TheoremRelationship between the coefficients and the roots of a split polynomial#

Vieta's formula for the coefficients and the roots of a polynomial over an integral domain with as many roots as its degree.

Polynomial.coeff_eq_esymm_roots_of_card.{u_1} {R : Type u_1} [CommRing R] [IsDomain R]
  {p : Polynomial R} (hroots : p.roots.card = p.natDegree) {k : ℕ} (h : k ≤ p.natDegree) :
  p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Sources

• Mathlib documentation: Polynomial.coeff_eq_esymm_roots_of_card
• Source of Polynomial.coeff_eq_esymm_roots_of_card in Mathlib/RingTheory/Polynomial/Vieta.lean
• Mathlib undergraduate list: Ring Theory › Polynomial rings

MathlibPolynomial.coeff_eq_esymm_roots_of_card

Uses 2

Statement usesRoots of a polynomial

Proof usesVieta's formulas

TheoremNewton's identities#

Newton's identities give a recurrence relation for the kth elementary symmetric polynomial in terms of lower degree elementary symmetric polynomials and power sums.

MvPolynomial.mul_esymm_eq_sum.{u_1, u_2} (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R]
  (k : ℕ) :
  ↑k * MvPolynomial.esymm σ R k =
    (-1) ^ (k + 1) *
      ∑ a ∈ Finset.HasAntidiagonal.antidiagonal k with a.1 < k,
        (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2

Sources

• Mathlib documentation: MvPolynomial.mul_esymm_eq_sum
• Source of MvPolynomial.mul_esymm_eq_sum in Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
• Mathlib undergraduate list: Ring Theory › Polynomial rings

MathlibMvPolynomial.mul_esymm_eq_sum

Uses 4

Statement usesInteger · Linear map · Polynomial in several indeterminates

Proof usesFormula for the Number of Combinations

DefinitionPolynomial derivative#

derivative p is the formal derivative of the polynomial p

Polynomial.derivative.{u} {R : Type u} [Semiring R] : Polynomial R →ₗ[R] Polynomial R

Sources

• Mathlib documentation: Polynomial.derivative
• Source of Polynomial.derivative in Mathlib/Algebra/Polynomial/Derivative.lean
• Mathlib undergraduate list: Ring Theory › Polynomial rings

MathlibPolynomial.derivative

Uses 2 · Used by 6

Statement usesLinear map · Polynomial in one indeterminate

Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Hensel's lemma (for \(\mathbb{Z}_p\)) · Multiplicity · Separable polynomial · Mason–Stothers theorem · Gauss–Lucas theorem

TheoremDecomposition into sums of homogeneous polynomials#

Mathlib states this as MvPolynomial.sum_homogeneousComponent.

MvPolynomial.sum_homogeneousComponent.{u_1, u_3} {σ : Type u_1} {R : Type u_3} [CommSemiring R]
  (φ : MvPolynomial σ R) :
  ∑ i ∈ Finset.range (φ.totalDegree + 1), (MvPolynomial.homogeneousComponent i) φ = φ

Sources

• Mathlib documentation: MvPolynomial.sum_homogeneousComponent
• Source of MvPolynomial.sum_homogeneousComponent in Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
• Mathlib undergraduate list: Ring Theory › Polynomial rings

MathlibMvPolynomial.sum_homogeneousComponent

Uses 2

Statement usesLinear map · Polynomial in several indeterminates

DefinitionSymmetric polynomials#

A MvPolynomial φ is symmetric if it is invariant under permutations of its variables by the rename operation

MvPolynomial.IsSymmetric.{u_1, u_3} {σ : Type u_1} {R : Type u_3} [CommSemiring R]
  (φ : MvPolynomial σ R) : Prop

Sources

• Mathlib documentation: MvPolynomial.IsSymmetric
• Source of MvPolynomial.IsSymmetric in Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
• Mathlib undergraduate list: Ring Theory › Polynomial rings

MathlibMvPolynomial.IsSymmetric

Uses 2

Statement usesAssociative algebra over a commutative ring · Polynomial in several indeterminates

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.