Revision #1480 → #1782 · back to history
modifiedEvaluation by substitutione15664577f64
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Notation and terminology","snippet":"denotes, by convention, the result of substituting"},{"type":"math_alttext","value":"{\\displaystyle a\\mapsto P(a),}"}] | — |
modifiedSubstituting the indeterminate yields the polynomialf61dba747e74
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Notation and terminology","snippet":"does not change anything"},{"type":"math_alttext","value":"{\\displaystyle P(x)=P,}"}] | — |
modifiedStandard form of a univariate polynomial550bca60f32d
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Definition","snippet":"A polynomial in a single indeterminate x can always be written"},{"type":"math_alttext","value":"{\\displaystyle a_{n}x^{n}+a_{n-1}x^{n-1}+\\dotsb +a_{2}x^{2}+a_{1}x+a_{0},}"}] | — |
modifiedLeading coefficienta1b93755976f
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Definition","snippet":"The leading coefficient of such a polynomial is"},{"type":"math_alttext","value":"{\\displaystyle a_{n}x^{n}+a_{n-1}x^{n-1}+\\dotsb +a_{2}x^{2}+a_{1}x+a_{0},}"}] | — |
modifiedPolynomial as finite sum of termsf03be1326ce4
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Definition","snippet":"a polynomial can either be zero or can be written as the sum of a finite number of non-zero terms"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{n}a_{k}x^{k}}"}] | — |
modifiedConstant term and constant polynomiald3cb483d420f
| Field | From #1480 | To #1782 |
|---|
| mathlib.decl | Polynomial.constantCoeff | Polynomial.C |
| mathlib.module | Mathlib.Algebra.Polynomial.Coeff | Mathlib.Algebra.Polynomial.Basic |
| note | `Polynomial.constantCoeff` is the constant term and `Polynomial.C` embeds constant polynomials. | `Polynomial.C` embeds the coefficient ring as constant polynomials; the constant term of `p` is `p.coeff 0`. |
| provenance | ai | ai-moderated |
modifiedDegree of a term005c8a0193a8
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Classification","snippet":"is a term. The coefficient is"},{"type":"math_alttext","value":"{\\displaystyle -5x^{2}y}"}] | — |
modifiedPolynomial as sum of three termscd1603710ae3
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Classification","snippet":"Forming a sum of several terms produces a polynomial."},{"type":"math_alttext","value":"{\\displaystyle \\underbrace {_{\\,}3x^{2}} _{\\begin{smallmatrix}\\mathrm {term} \\\\\\mathrm {1} \\end{smallmatrix}}\\underbrace {-_{\\,}5x} _{\\begin{smallmatrix}\\mathrm {term} \\\\\\mathrm {2} \\end{smallmatrix}}\\underbrace {+_{\\,}4} _{\\begin{smallmatrix}\\mathrm {term} \\\\\\mathrm {3} \\end{smallmatrix}}.}"}] | — |
modifiedAddition of polynomials038d5db3791d
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Addition and subtraction","snippet":"Polynomials can be added using the associative law of addition"},{"type":"math_alttext","value":"{\\displaystyle P=3x^{2}-2x+5xy-2}"},{"type":"math_alttext","value":"{\\displaystyle Q=-3x^{2}+3x+4y^{2}+8}"},{"type":"math_alttext","value":"{\\displaystyle P+Q=3x^{2}-2x+5xy-2-3x^{2}+3x+4y^{2}+8}"},{"type":"math_alttext","value":"{\\displaystyle P+Q=(3x^{2}-3x^{2})+(-2x+3x)+5xy+4y^{2}+(8-2)}"},{"type":"math_alttext","value":"{\\displaystyle P+Q=x+5xy+4y^{2}+6.}"}] | — |
modifiedMultiplication of polynomialsb6d1661cbccd
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Multiplication","snippet":"Polynomials can also be multiplied."},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\color {Red}P\\,&\\color {Red}{=2x+3y+5}\\\\\\color {Blue}Q\\,&{\\color {Blue}{=2x+5y+xy+1}},\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{array}{rccrcrcrcr}{\\color {Red}{P}}{\\color {Blue}{Q}}&{=}&&({\\color {Red}{2x}}\\cdot {\\color {Blue}{2x}})&+&({\\color {Red}{2x}}\\cdot {\\color {Blue}{5y}})&+&({\\color {Red}{2x}}\\cdot {\\color {Blue}{xy}})&+&({\\color {Red}{2x}}\\cdot {\\color {Blue}{1}})\\\\&&+&({\\color {Red}{3y}}\\cdot {\\color {Blue}{2x}})&+&({\\color {Red}{3y}}\\cdot {\\color {Blue}{5y}})&+&({\\color {Red}{3y}}\\cdot {\\color {Blue}{xy}})&+&({\\color {Red}{3y}}\\cdot {\\color {Blue}{1}})\\\\&&+&({\\color {Red}{5}}\\cdot {\\color {Blue}{2x}})&+&({\\color {Red}{5}}\\cdot {\\color {Blue}{5y}})&+&({\\color {Red}{5}}\\cdot {\\color {Blue}{xy}})&+&({\\color {Red}{5}}\\cdot {\\color {Blue}{1}})\\end{array}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{array}{rccrcrcrcr}PQ&=&&4x^{2}&+&10xy&+&2x^{2}y&+&2x\\\\&&+&6xy&+&15y^{2}&+&3xy^{2}&+&3y\\\\&&+&10x&+&25y&+&5xy&+&5.\\end{array}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{array}{rcccrcrcrcr}PQ&=&&4x^{2}&+&(10xy+6xy+5xy)&+&2x^{2}y&+&(2x+10x)\\\\&&+&15y^{2}&+&3xy^{2}&+&(3y+25y)&+&5\\end{array}}}"},{"type":"math_alttext","value":"{\\displaystyle PQ=4x^{2}+21xy+2x^{2}y+12x+15y^{2}+3xy^{2}+28y+5.}"}] | — |
modifiedComposition of polynomialsaf526ad8bd01
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Composition","snippet":"is obtained by substituting each copy of the variable of the first polynomial by the second polynomial"},{"type":"math_alttext","value":"{\\displaystyle (f\\circ g)(x)=f(g(x))=(3x+2)^{2}+2(3x+2).}"}] | — |
modifiedFactorization into irreducible polynomials24321a1122d9
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Factoring","snippet":"also have a factored form in which the polynomial is written as a product of irreducible polynomials and a constant"},{"type":"math_alttext","value":"{\\displaystyle 5x^{3}-5}"},{"type":"math_alttext","value":"{\\displaystyle 5(x-1)\\left(x^{2}+x+1\\right)}"},{"type":"math_alttext","value":"{\\displaystyle 5(x-1)\\left(x+{\\frac {1+i{\\sqrt {3}}}{2}}\\right)\\left(x+{\\frac {1-i{\\sqrt {3}}}{2}}\\right)}"}] | — |
modifiedDerivative of a polynomial8150ffd4c151
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Calculus","snippet":"The derivative of the polynomial"},{"type":"math_alttext","value":"{\\displaystyle P=a_{n}x^{n}+a_{n-1}x^{n-1}+\\dots +a_{2}x^{2}+a_{1}x+a_{0}=\\sum _{i=0}^{n}a_{i}x^{i}}"},{"type":"math_alttext","value":"{\\displaystyle na_{n}x^{n-1}+(n-1)a_{n-1}x^{n-2}+\\dots +2a_{2}x+a_{1}=\\sum _{i=1}^{n}ia_{i}x^{i-1}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {a_{n}x^{n+1}}{n+1}}+{\\frac {a_{n-1}x^{n}}{n}}+\\dots +{\\frac {a_{2}x^{3}}{3}}+{\\frac {a_{1}x^{2}}{2}}+a_{0}x+c=c+\\sum _{i=0}^{n}{\\frac {a_{i}x^{i+1}}{i+1}}}"}] | — |
modifiedAntiderivative of a polynomial1fba3a5e7be4
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Calculus","snippet":"the general antiderivative (or indefinite integral)"},{"type":"math_alttext","value":"{\\displaystyle P=a_{n}x^{n}+a_{n-1}x^{n-1}+\\dots +a_{2}x^{2}+a_{1}x+a_{0}=\\sum _{i=0}^{n}a_{i}x^{i}}"},{"type":"math_alttext","value":"{\\displaystyle na_{n}x^{n-1}+(n-1)a_{n-1}x^{n-2}+\\dots +2a_{2}x+a_{1}=\\sum _{i=1}^{n}ia_{i}x^{i-1}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {a_{n}x^{n+1}}{n+1}}+{\\frac {a_{n-1}x^{n}}{n}}+\\dots +{\\frac {a_{2}x^{3}}{3}}+{\\frac {a_{1}x^{2}}{2}}+a_{0}x+c=c+\\sum _{i=0}^{n}{\\frac {a_{i}x^{i+1}}{i+1}}}"}] | — |
modifiedPolynomial function6d622ea2389c
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Polynomial functions","snippet":"A polynomial function is a function defined by evaluating a polynomial."},{"type":"math_alttext","value":"{\\displaystyle a_{n}x^{n}+a_{n-1}x^{n-1}+\\cdots +a_{2}x^{2}+a_{1}x+a_{0}}"}] | — |
modifiedPolynomial function of one variabled50d763cf349
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Polynomial functions","snippet":"is a polynomial function of one variable"},{"type":"math_alttext","value":"{\\displaystyle f(x)=x^{3}-x,}"},{"type":"math_alttext","value":"{\\displaystyle f(x,y)=2x^{3}+4x^{2}y+xy^{5}+y^{2}-7.}"}] | — |
modifiedHorner's method9b8695610d07
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Polynomial functions","snippet":"using Horner's method"},{"type":"math_alttext","value":"{\\displaystyle (((((a_{n}x+a_{n-1})x+a_{n-2})x+\\dotsb +a_{3})x+a_{2})x+a_{1})x+a_{0}.}"}] | — |
modifiedPolynomial equationded7cd07f453
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Equations","snippet":"A polynomial equation , also called an algebraic equation , is an equation of the form"},{"type":"math_alttext","value":"{\\displaystyle a_{n}x^{n}+a_{n-1}x^{n-1}+\\dotsb +a_{2}x^{2}+a_{1}x+a_{0}=0.}"},{"type":"math_alttext","value":"{\\displaystyle 3x^{2}+4x-5=0}"}] | — |
modifiedZeros of multivariate polynomials84d7d6b07a03
| Field | From #1480 | To #1782 |
|---|
| mathlib.module | Mathlib.Algebra.MvPolynomial.Basic | Mathlib.Algebra.MvPolynomial.Eval |
modifiedMatrix polynomial0d2a63899084
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Matrix polynomials","snippet":"A matrix polynomial is a polynomial with square matrices as variables."},{"type":"math_alttext","value":"{\\displaystyle P(x)=\\sum _{i=0}^{n}{a_{i}x^{i}}=a_{0}+a_{1}x+a_{2}x^{2}+\\cdots +a_{n}x^{n},}"},{"type":"math_alttext","value":"{\\displaystyle P(A)=\\sum _{i=0}^{n}{a_{i}A^{i}}=a_{0}I+a_{1}A+a_{2}A^{2}+\\cdots +a_{n}A^{n},}"}] | — |
| mathlib.module | Mathlib.LinearAlgebra.Matrix.Charpoly.Basic | Mathlib.RingTheory.MatrixPolynomialAlgebra |
modifiedMultivariate reduces to iterated univariatef003ae24d8e6
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Polynomial ring","snippet":"most of the theory of the multivariate case can be reduced to an iterated univariate case"},{"type":"math_alttext","value":"{\\displaystyle R[x_{1},\\ldots ,x_{n}]=\\left(R[x_{1},\\ldots ,x_{n-1}]\\right)[x_{n}].}"}] | — |
modifiedEuclidean division; F[x] is a Euclidean domain07c8f4a8f51a
| Field | From #1480 | To #1782 |
|---|
| anchors | [{"section":"Divisibility","snippet":"shows that the ring F [ x ] is a Euclidean domain"},{"type":"math_alttext","value":"{\\displaystyle f=q\\,g+r}"}] | — |
addedEisenstein's criteriondc2d843384af
addedPolynomial interpolation (Lagrange)0fdd56dad81f