Polynomial.coe_mapRingHom
theorem Polynomial.coe_mapRingHom :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
⇑(Polynomial.mapRingHom f) = Polynomial.map f
This theorem states that for any two types `R` and `S`, both equipped with a semiring structure, and any ring homomorphism `f` from `R` to `S`, the application of the `Polynomial.mapRingHom` function to `f` is equal to the `Polynomial.map` function applied to `f`. In other words, the `Polynomial.mapRingHom` and `Polynomial.map` functions are consistent with each other when dealing with ring homomorphisms.
More concisely: For any semiring homomorphisms `f` between types `R` and `S`, `Polynomial.mapRingHom f = Polynomial.map f`.
|
Polynomial.eval₂_monomial
theorem Polynomial.eval₂_monomial :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) {n : ℕ} {r : R},
Polynomial.eval₂ f x ((Polynomial.monomial n) r) = f r * x ^ n
The theorem `Polynomial.eval₂_monomial` states that for any semirings `R` and `S`, given a ring homomorphism `f` from `R` to `S`, a scalar `x` in `S`, a natural number `n` and a scalar `r` in `R`, evaluating the monomial `a * X^n` at `x` using `f` is equivalent to applying `f` to `a` and multiplying the result by `x` raised to the power `n`. In other words, `f(a) * x^n` is the evaluation of the monomial `a * X^n` under the mapping `f` and the value `x`.
More concisely: For any semirings R and S, ring homomorphism f from R to S, scalar x in S, natural number n, and scalar r in R, we have f(ar^n) = a * (xf^n).
|
Polynomial.eval_eq_sum_range
theorem Polynomial.eval_eq_sum_range :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (x : R),
Polynomial.eval x p = (Finset.range (p.natDegree + 1)).sum fun i => p.coeff i * x ^ i
The theorem `Polynomial.eval_eq_sum_range` states that for any semiring `R` and any polynomial `p` of type `R`, the evaluation of the polynomial `p` at a point `x` in `R` is equal to the sum over the range from 0 to the natural degree of `p` (inclusive) of the `i`-th coefficient of `p` times `x` raised to the `i`-th power. In other words, the polynomial evaluation at `x` is the sum of each term's contribution at `x`, where each term is the product of the coefficient of the term and `x` raised to the power equal to the degree of the term, which is essentially the definition of polynomial evaluation in a semiring.
More concisely: For any semiring `R` and polynomial `p` of type `R`, the evaluation of `p` at a point `x` in `R` equals the sum of the products of each `i`-th coefficient of `p` with `x` raised to the power `i`, from `i` equal to `0` to the natural degree of `p`.
|
Polynomial.eval₂_one
theorem Polynomial.eval₂_one :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S),
Polynomial.eval₂ f x 1 = 1
The theorem `Polynomial.eval₂_one` states that for any semiring `R` and `S`, and for any ring homomorphism `f` from `R` to `S`, and for any value `x` in `S`, the evaluation of the polynomial `1` (which is a constant polynomial with value `1`) at `x` using the ring homomorphism `f` is `1`. This is to say, regardless of the ring homomorphism and the value for the variable, the evaluation of the constant polynomial `1` is always `1`.
More concisely: For any semiring R and ring homomorphism f from R to S, f(1\_R) = 1\_S, where 1\_R is the constant polynomial with value 1 in R and 1\_S is the constant value 1 in S.
|
Polynomial.eval_C
theorem Polynomial.eval_C :
∀ {R : Type u} {a : R} [inst : Semiring R] {x : R}, Polynomial.eval x (Polynomial.C a) = a
The theorem `Polynomial.eval_C` states that, for any semiring `R`, any element `a` of `R`, and any element `x` of `R`, the evaluation of the constant polynomial `a` (represented by `Polynomial.C a`) at `x` is always equal to `a`. In other words, the value of a constant polynomial doesn't change under evaluation at any point in the semiring.
More concisely: For any semiring R and its elements a and x, the constant polynomial C(a) of R evaluates to a at x.
|
Polynomial.eval_monomial
theorem Polynomial.eval_monomial :
∀ {R : Type u} [inst : Semiring R] {x : R} {n : ℕ} {a : R},
Polynomial.eval x ((Polynomial.monomial n) a) = a * x ^ n
This theorem states that for any type `R` equipped with a semiring structure, any instance `x` of `R`, any natural number `n`, and any instance `a` of `R`, the evaluation of the polynomial `(Polynomial.monomial n) a` at `x` is equal to `a * x ^ n`. In other words, if you have a polynomial that is just a single term `a * X^n`, and you substitute `x` for `X`, you get `a * x^n`. This is a fundamental property reflecting how polynomials behave under substitution.
More concisely: For any semiring `R`, `x : R`, natural number `n`, and `a : R`, the evaluation of the monomial `(Polynomial.monomial n) a` at `x` equals `a * x^n`.
|
Polynomial.eval_add
theorem Polynomial.eval_add :
∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {x : R},
Polynomial.eval x (p + q) = Polynomial.eval x p + Polynomial.eval x q
The theorem `Polynomial.eval_add` states that for any type `R` which is a semiring, for any polynomials `p` and `q` over `R`, and for any element `x` of `R`, the evaluation of the sum of `p` and `q` at `x` is equivalent to the sum of the evaluation of `p` at `x` and the evaluation of `q` at `x`. In mathematical terms, this theorem asserts the linearity of polynomial evaluation: `eval(x, p + q) = eval(x, p) + eval(x, q)`, which is a fundamental property in algebra.
More concisely: For any semiring `R`, polynomial `p` and `q` over `R`, and `x` in `R`, `eval(x, p + q) = eval(x, p) + eval(x, q)`.
|
Polynomial.coeff_map
theorem Polynomial.coeff_map :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ),
(Polynomial.map f p).coeff n = f (p.coeff n)
The theorem `Polynomial.coeff_map` states that for any semirings `R` and `S`, any polynomial `p` of type `Polynomial R`, any ring homomorphism `f` from `R` to `S`, and any natural number `n`, the coefficient of `X^n` in the polynomial obtained by mapping `p` across `f` is equal to the result of applying `f` to the coefficient of `X^n` in `p`. In other words, if you map a polynomial to another ring using a ring hom, the coefficients of the resulting polynomial are just the images under the hom of the coefficients of the original polynomial.
More concisely: For any semirings R and S, ring homomorphism f from R to S, polynomial p of type Polynomial R over X, and natural number n, the coefficient of X^n in the polynomial f(p) obtained by mapping p across f is equal to f(coeff p X^n).
|
Polynomial.eval₂_eq_sum
theorem Polynomial.eval₂_eq_sum :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S} {x : S},
Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
The theorem `Polynomial.eval₂_eq_sum` states that for all semirings `R` and `S`, a polynomial `p` of type `R`, a ring homomorphism `f` from `R` to `S`, and a value `x` of type `S`, the evaluation of the polynomial `p` using the ring homomorphism `f` and variable value `x` (through the function `Polynomial.eval₂`) is equal to the sum (through the function `Polynomial.sum`) of the values obtained by applying a function to the coefficients of the polynomial, where this function multiplies the image of the coefficient under `f` with the variable `x` raised to the power of the coefficient's degree (`f a * x ^ e`). In other words, this theorem provides a specific method to compute the evaluation of a polynomial by summing over its coefficients.
More concisely: For all semirings R and S, polynomial p of type R, ring homomorphism f from R to S, and value x of type S, the evaluation of p using f and x is equal to the sum of the products of the images of the polynomial coefficients under f and x raised to their degrees.
|
Polynomial.coeff_zero_eq_eval_zero
theorem Polynomial.coeff_zero_eq_eval_zero :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.coeff 0 = Polynomial.eval 0 p
This theorem states that for any polynomial `p` over a semiring `R`, the coefficient of the term with zero degree in the polynomial, denoted by `Polynomial.coeff p 0`, is equal to the value of the polynomial evaluated at zero, denoted by `Polynomial.eval 0 p`. This corresponds to the familiar fact from algebra that the constant term of a polynomial is the value of the polynomial when all its variables are set to zero.
More concisely: For any polynomial `p` over a semiring `R`, the constant term `Polynomial.coeff p 0` is equal to `Polynomial.eval 0 p`.
|
Polynomial.comp_C
theorem Polynomial.comp_C :
∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
p.comp (Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
This theorem states that for any type `R` which forms a semiring, for any element `a` of `R`, and for any polynomial `p` with coefficients from `R`, the composition of the polynomial `p` with the constant polynomial `a` is the same as the constant polynomial whose value is the evaluation of `p` at `a`. In mathematical terms, it says that the composition of a polynomial `p(x)` with a constant `a`, denoted as `p(a)`, is a constant polynomial whose value is `p(a)`.
More concisely: For any semiring `R`, any element `a` in `R`, and any polynomial `p(x)` with coefficients in `R`, `p(a)` is the constant polynomial equal to the value of `p` evaluated at `a`.
|
Polynomial.map_monomial
theorem Polynomial.map_monomial :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {n : ℕ} {a : R},
Polynomial.map f ((Polynomial.monomial n) a) = (Polynomial.monomial n) (f a)
The theorem `Polynomial.map_monomial` states that for any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, and any natural number `n` and element `a` of `R`, the result of mapping the polynomial `a * X^n` (`a` times `X` raised to the power `n`) across the ring homomorphism `f` is the same as the polynomial obtained by first applying the ring homomorphism `f` to `a` and then multiplying the result by `X` raised to the power `n`. In other words, this theorem asserts that the process of applying a ring homomorphism to a polynomial is commutative with the process of forming a monomial.
More concisely: For any semirings R and S, ring homomorphism f from R to S, natural number n, and element a in R, we have f(a * X^n) = f(a) * X^n.
|
Polynomial.X_comp
theorem Polynomial.X_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.X.comp p = p
This theorem states that for any type `R` with a semiring structure and any polynomial `p` over `R`, the composition of the polynomial `p` with the polynomial variable, denoted `Polynomial.X`, is equal to `p` itself. In other words, if we substitute the polynomial variable into `p` everywhere, the result is `p`. This can be thought of as the polynomial version of the identity function, familiar from basic algebra: substituting `x` into a function `f(x)` everywhere just gives back `f(x)`.
More concisely: For any semiring `R` and polynomial `p` over `R`, `p * Polynomial.X = p`.
|
Polynomial.map_X
theorem Polynomial.map_X :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
Polynomial.map f Polynomial.X = Polynomial.X
The theorem `Polynomial.map_X` states that for any two types `R` and `S` that are semirings, and any ring homomorphism `f` from `R` to `S`, applying the map function to the polynomial variable `Polynomial.X` in `R` results in the polynomial variable `Polynomial.X` in `S`. In other words, the variable (indeterminate) of the polynomial remains the same even when the coefficients are mapped across a ring homomorphism.
More concisely: For any semirings R and S and ring homomorphism f from R to S, the map function applied to Polynomial.X in R is equal to Polynomial.X in S.
|
Polynomial.eval₂_mul
theorem Polynomial.eval₂_mul :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S)
(x : S), Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
This theorem, `Polynomial.eval₂_mul`, states that for any two polynomials `p` and `q` over a semiring `R`, and any ring homomorphism `f` from `R` to a commutative semiring `S`, and any value `x` in `S`, the evaluation of the product of `p` and `q` under `f` at `x` is equal to the product of the evaluations of `p` and `q` under `f` at `x`. In other words, it says that the function `Polynomial.eval₂ f x` preserves multiplication, which is a fundamental property required of a ring homomorphism. It is expressed mathematically as
\[
\text{Polynomial.eval₂}\ f\ x\ (p \times q) = \text{Polynomial.eval₂}\ f\ x\ p \times \text{Polynomial.eval₂}\ f\ x\ q
\]
More concisely: For any semiring homomorphism $f$ from a semiring $R$ to a commutative semiring $S$ and any polynomials $p, q$ over $R$, the evaluation of their product under $f$ at any value $x$ in $S$ equals the product of their individual evaluations: $\text{Polynomial.eval₂}\ f\ x\ (p \times q) = \text{Polynomial.eval₂}\ f\ x\ p \times \text{Polynomial.eval₂}\ f\ x\ q$.
|
Polynomial.eval₂_X
theorem Polynomial.eval₂_X :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S),
Polynomial.eval₂ f x Polynomial.X = x
This theorem states that for any semiring `R` and any semiring `S`, given a ring homomorphism `f` from `R` to `S` and an element `x` of `S`, the evaluation of the polynomial `X` (the polynomial variable or indeterminate) in `S` using the evaluation map `eval₂` with `f` and `x` is equal to `x` itself. In other words, it says that substituting the indeterminate in the polynomial `X` with a value `x` from the semiring `S` results in that value `x`.
More concisely: For any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, and any element `x` in `S`, the evaluation of the polynomial `X` in `S` using `eval₂` with `f` and `x` equals `x`.
|
Polynomial.mul_comp
theorem Polynomial.mul_comp :
∀ {R : Type u_1} [inst : CommSemiring R] (p q r : Polynomial R), (p * q).comp r = p.comp r * q.comp r
The theorem `Polynomial.mul_comp` states that for any given type `R` which forms a commutative semiring, and for any three polynomials `p`, `q`, and `r` over type `R`, the result of composing the product of `p` and `q` with `r` is equal to the product of the result of composing `p` with `r` and the result of composing `q` with `r`. This can be expressed as: `Polyomial.comp (p * q) r = Polyomial.comp p r * Polyomial.comp q r`. This theorem essentially demonstrates the distributive property of polynomial composition over multiplication.
More concisely: For any commutative semiring type R and polynomials p, q, and r over R, the distribution law holds: Polyomial.comp (p * q) r = Polyomial.comp p r * Polyomial.comp q r.
|
Polynomial.eval_pow
theorem Polynomial.eval_pow :
∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R} {x : R} (n : ℕ),
Polynomial.eval x (p ^ n) = Polynomial.eval x p ^ n
The theorem `Polynomial.eval_pow` states that for any commutative semiring `R`, any polynomial `p` of type `Polynomial R`, any element `x` of `R`, and any natural number `n`, the evaluation of `p` raised to the power `n` at `x` is equal to the evaluation of `p` at `x` raised to the power `n`. In other words, it asserts that the evaluation function for polynomials respects exponentiation, which can be expressed in mathematical notation as $eval(x, p^n) = (eval(x, p))^n$.
More concisely: For any commutative semiring R, polynomial p of type Polynomial R, element x of R, and natural number n, the evaluation of p raised to the power n at x equals the power of the evaluation of p at x, i.e., eval(x, p^n) = (eval x p)^n.
|
Polynomial.eval₂_add
theorem Polynomial.eval₂_add :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
Polynomial.eval₂ f x (p + q) = Polynomial.eval₂ f x p + Polynomial.eval₂ f x q
This theorem, `Polynomial.eval₂_add`, states that for any two polynomials `p` and `q` over a semiring `R`, a ring homomorphism `f` from `R` to another semiring `S`, and an element `x` in `S`, the evaluation of the sum `p + q` at `x` via `f` (denoted as `Polynomial.eval₂ f x (p + q)`) is equal to the sum of the evaluations of `p` and `q` at `x` via `f` (denoted as `Polynomial.eval₂ f x p + Polynomial.eval₂ f x q`). In other words, it states that the evaluation function for polynomials respects addition.
More concisely: For any semirings R and S, ring homomorphism f from R to S, and polynomials p and q over R, the evaluation of p + q at x via f is equal to the sum of the evaluations of p and q at x via f.
|
Polynomial.eval_neg
theorem Polynomial.eval_neg :
∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (x : R), Polynomial.eval x (-p) = -Polynomial.eval x p
The theorem `Polynomial.eval_neg` states that for all rings `R`, for any polynomial `p` of `R`, and for any element `x` from `R`, the evaluation of the negation of the polynomial `p` at `x` is equal to the negation of the evaluation of the polynomial `p` at `x`. In mathematical terms, this can be written as \(-p(x) = -f(x)\), where \(p(x)\) is the evaluation of the polynomial function \(f\) at \(x\).
More concisely: For all rings R, polynomials p of R, and elements x of R, -(p x) = -(px).
|
Polynomial.eval₂_at_apply
theorem Polynomial.eval₂_at_apply :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Semiring S] (f : R →+* S) (r : R),
Polynomial.eval₂ f (f r) p = f (Polynomial.eval r p)
The theorem `Polynomial.eval₂_at_apply` states that for any semiring `R`, any polynomial `p` from `R`, any semiring `S`, any ring homomorphism `f` from `R` to `S`, and any element `r` of `R`, evaluating `p` at `r` (under the ring homomorphism `f`) is the same as applying `f` to the result of evaluating `p` at `r`. In terms of mathematical notation, this theorem states that for all `f : R →+* S` and `r ∈ R`, we have `f(p(r)) = p(f(r))`.
More concisely: For any semiring homomorphism $f$ and element $r$ in a semiring, we have $f(p(r)) = p(f(r))$ for all polynomials $p$ over the semiring.
|
Polynomial.eval_C_mul
theorem Polynomial.eval_C_mul :
∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} {x : R},
Polynomial.eval x (Polynomial.C a * p) = a * Polynomial.eval x p
The theorem `Polynomial.eval_C_mul` states that for any type `R` equipped with a semiring structure, a given element `a` of `R`, a polynomial `p` over `R`, and a value `x` from `R`, the evaluation of the multiplication of the constant polynomial `a` and `p` at `x` is the same as the product of `a` and the evaluation of `p` at `x`. In other words, if we multiply a polynomial by a constant and then evaluate it at a point, it's the same as if we evaluated the polynomial first and then multiplied the result by the constant. This is denoted in mathematical terms as `Polynomial.eval x (Polynomial.C a * p) = a * Polynomial.eval x p`.
More concisely: For any semiring `R`, polynomial `p` over `R`, constant `a` in `R`, and `x` in `R`, `Polynomial.eval x (Polynomial.C a * p) = a * Polynomial.eval x p`.
|
Polynomial.map_id
theorem Polynomial.map_id :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.map (RingHom.id R) p = p
This theorem states that for any semiring `R` and any polynomial `p` over this ring, if we apply the function `Polynomial.map` with the identity ring homomorphism `RingHom.id R` to `p`, we get `p` itself. In other words, mapping a polynomial across the identity ring homomorphism leaves the polynomial unchanged.
More concisely: For any semiring `R` and polynomial `p` over `R`, applying the identity ring homomorphism `RingHom.id R` to `p` via `Polynomial.map` results in `p` itself.
|
Polynomial.map_pow
theorem Polynomial.map_pow :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ),
Polynomial.map f (p ^ n) = Polynomial.map f p ^ n
The theorem `Polynomial.map_pow` states that for any semiring `R` and `S`, any polynomial `p` of type `R`, any ring homomorphism `f` from `R` to `S`, and any natural number `n`, mapping the `n`th power of `p` across `f` is the same as the `n`th power of the mapped `p` across `f`. In other words, the operation of mapping a polynomial across a ring homomorphism commutes with taking powers of polynomials.
More concisely: For any semiring R, ring homomorphism f from R to S, polynomial p of type R, and natural number n, the mapped polynomial f(p^n) equals the n-th power of the mapped polynomial f(p) in S.
|
Polynomial.hom_eval₂
theorem Polynomial.hom_eval₂ :
∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] (p : Polynomial R) [inst_1 : Semiring S]
[inst_2 : Semiring T] (f : R →+* S) (g : S →+* T) (x : S),
g (Polynomial.eval₂ f x p) = Polynomial.eval₂ (g.comp f) (g x) p
This theorem states that for any semirings `R`, `S`, and `T`, a polynomial `p` with coefficients in `R`, a ring homomorphism `f` from `R` to `S`, another ring homomorphism `g` from `S` to `T`, and an element `x` of `S`, the result of first applying the evaluation function `eval₂` to `f`, `x`, and `p` (which evaluates `p` at `x` after applying `f` to the coefficients of `p`), and then applying `g` to the result, is equal to the result of applying the evaluation function `eval₂` to the composition of `g` and `f`, `g(x)`, and `p`. This illustrates the compatibility of the polynomial evaluation process with the composition of ring homomorphisms.
More concisely: For any semirings R, S, T, ring homomorphisms f : R -> S and g : S -> T, polynomial p with coefficients in R, and element x in S, the application of g to the evaluation of p at x after applying f to its coefficients is equal to the evaluation of p at g(x) through the composition of f and g.
|
Polynomial.zero_comp
theorem Polynomial.zero_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.comp 0 p = 0 := by
sorry
This theorem states that for any semiring `R` and any polynomial `p` over `R`, the composition of the zero polynomial with `p` results in the zero polynomial. In other words, if we substitute `p` into the zero polynomial, we get back the zero polynomial. This is like saying that applying any function to zero gives us zero, but in the context of polynomial composition.
More concisely: For any semiring `R` and polynomial `p` over `R`, the zero polynomial composed with `p` equals the zero polynomial.
|
Polynomial.eval₂_pow
theorem Polynomial.eval₂_pow :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (x : S)
(n : ℕ), Polynomial.eval₂ f x (p ^ n) = Polynomial.eval₂ f x p ^ n
This theorem states that for any two types `R` and `S` with `R` being a semiring and `S` being a commutative semiring, given a ring homomorphism `f` from `R` to `S`, a value `x` in `S`, a polynomial `p` over `R`, and a natural number `n`, the evaluation of the `n`-th power of the polynomial `p` at `x` (using the ring homomorphism `f` to map the coefficients into `S`) is equal to the `n`-th power of the evaluation of `p` at `x`. In mathematical notation, if we denote the evaluation of a polynomial `p` at `x` with ring homomorphism `f` as `eval₂(f, x, p)`, then the theorem states that `eval₂(f, x, p^n) = eval₂(f, x, p)^n`.
More concisely: For any semiring homomorphism \(f\) from semiring \(R\) to commutative semiring \(S\), and for any \(x \in S\), polynomial \(p \in R[\underline{x}]\), and natural number \(n\), we have \(f(p^n)(x) = (f(p))^n(x)\).
|
Polynomial.map_add
theorem Polynomial.map_add :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
Polynomial.map f (p + q) = Polynomial.map f p + Polynomial.map f q
The theorem `Polynomial.map_add` states that for any two polynomials `p` and `q` over a semiring `R`, and a ring homomorphism `f` from `R` to another semiring `S`, the map of the sum of `p` and `q` under `f` equals to the sum of the maps of `p` and `q` under `f`. In other words, the map operation preserves the addition operation of polynomials, which is a fundamental property related to the homomorphism between two algebraic structures.
More concisely: For any semiring homomorphism $f$ and polynomials $p, q$ over a semiring $R$, we have $f(p + q) = f(p) + f(q)$.
|
Polynomial.eval₂_def
theorem Polynomial.eval₂_def :
∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) (p : Polynomial R),
Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
The theorem `Polynomial.eval₂_def` states that for any semirings `R` and `S`, a ring homomorphism `f` from `R` to `S`, a scalar `x` in `S`, and a polynomial `p` with coefficients in `R`, the evaluation of the polynomial at `x` using `f` to map coefficients is equal to the sum of the product of the mapped coefficient and `x` raised to the power of the index, for each term in the polynomial. In other words, it expresses polynomial evaluation in terms of a sum over the terms of the polynomial.
More concisely: For any semirings R and S, ring homomorphism f from R to S, scalar x in S, and polynomial p with coefficients in R, the evaluation of p at x using f is equal to the sum of the products of the mapped coefficients and x raised to the corresponding powers for each term in p.
|
Polynomial.map_prod
theorem Polynomial.map_prod :
∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) {ι : Type u_1}
(g : ι → Polynomial R) (s : Finset ι),
Polynomial.map f (s.prod fun i => g i) = s.prod fun i => Polynomial.map f (g i)
The theorem `Polynomial.map_prod` states that for any commutative semiring `R` and `S`, and any ring homomorphism `f` from `R` to `S`, and any function `g` from a type `ι` to a Polynomial of `R`, and any finite set `s` of type `ι`, the map of the product of the polynomials `g i` for `i` in `s` under `f` is equal to the product of the maps of the polynomials `g i` under `f`. In other words, applying a ring homomorphism to the product of a set of polynomials is the same as taking the product of the individual polynomials each mapped by the ring homomorphism. This theorem is a statement of the property of ring homomorphisms preserving multiplication across the rings.
More concisely: For any commutative semirings R and S, ring homomorphism f from R to S, function g from a type ι to polynomials over R, and finite set s of type ι, the map of the product of g i for i in s under f is equal to the product of the maps of g i under f.
|
Polynomial.eval_zero
theorem Polynomial.eval_zero : ∀ {R : Type u} [inst : Semiring R] {x : R}, Polynomial.eval x 0 = 0
The theorem `Polynomial.eval_zero` states that for any given type `R` that forms a semiring, and for any element `x` of type `R`, the evaluation of the zero polynomial at `x` (i.e., `Polynomial.eval x 0`) is always zero. It essentially asserts the mathematical fact that if you substitute any number into the zero polynomial, the resulting value will be zero.
More concisely: For any semiring `R` and its element `x`, the value of the zero polynomial evaluated at `x` is zero.
|
Polynomial.eval_finset_sum
theorem Polynomial.eval_finset_sum :
∀ {R : Type u} {ι : Type y} [inst : Semiring R] (s : Finset ι) (g : ι → Polynomial R) (x : R),
Polynomial.eval x (s.sum fun i => g i) = s.sum fun i => Polynomial.eval x (g i)
The theorem `Polynomial.eval_finset_sum` states that for any given type `R` with a semiring structure, any finset `s` of type `ι`, a function `g` from `ι` to polynomials of `R`, and an element `x` of `R`, the evaluation of the sum of the polynomials (given by `g`) at `x` is equal to the sum of the evaluations of each polynomial (given by `g`) at `x`. In mathematical terms, for any finite set of indices and a function mapping each index to a specific polynomial, the value of the sum of these polynomials evaluated at a specific point is the same as the sum of the individual polynomial values at that point, i.e., $\text{eval}(x, \sum_{i\in s}{g(i)}) = \sum_{i\in s}{\text{eval}(x, g(i))}$.
More concisely: For any semiring `R`, finset `s` over index type `ι`, and function `g` from `ι` to polynomials of `R`, the evaluation of the sum of `g` at an element `x` of `R` is equal to the sum of the evaluations of each polynomial in `g` at `x`. In mathematical notation, $\text{eval}(x, \sum\_{i\in s}{g(i)}) = \sum\_{i\in s}{\text{eval}(x, g(i))}$.
|
Polynomial.eval_mul
theorem Polynomial.eval_mul :
∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {x : R},
Polynomial.eval x (p * q) = Polynomial.eval x p * Polynomial.eval x q
The theorem `Polynomial.eval_mul` states that for any commutative semiring `R`, any two polynomials `p` and `q` over `R`, and any element `x` of `R`, the value of the product of `p` and `q` evaluated at `x` is equal to the product of the values of `p` and `q` evaluated separately at `x`. This is essentially a statement of the distributive property of polynomial multiplication with respect to evaluation.
More concisely: For any commutative semiring R, polynomials p and q over R, and element x of R, (p * q) x = p x * q x.
|
Polynomial.map_injective
theorem Polynomial.map_injective :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
Function.Injective ⇑f → Function.Injective (Polynomial.map f)
The theorem `Polynomial.map_injective` states that for any two types `R` and `S`, where `R` and `S` are semirings, if a ring homomorphism `f` from `R` to `S` is injective, then the map of any polynomial from `R` to `S` using `f` is also injective. In other words, if `f` is such that whenever `f(x) = f(y)`, it follows that `x = y`, then for any polynomial `p` and `q`, if the `f`-image of `p` is equal to the `f`-image of `q`, it follows that `p = q`.
More concisely: If `f` is an injective ring homomorphism from semiring `R` to semiring `S`, then the map taking polynomials over `R` to their images under `f` is an injective homomorphism of `R`-algebras from the polynomial algebra over `R` to that over `S`.
|
Polynomial.map_map
theorem Polynomial.map_map :
∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S)
[inst_2 : Semiring T] (g : S →+* T) (p : Polynomial R),
Polynomial.map g (Polynomial.map f p) = Polynomial.map (g.comp f) p
The theorem `Polynomial.map_map` states that for all types `R`, `S`, and `T` which are semirings, and for all ring homomorphisms `f` from `R` to `S` and `g` from `S` to `T`, and for any polynomial `p` with coefficients in `R`, the process of first mapping `p` across `f` to get a polynomial in `S`, and then mapping the resultant polynomial across `g` to get a polynomial in `T`, is the same as the process of directly mapping `p` across the composition of `g` and `f`. This theorem essentially describes the property that the map operation on polynomials preserves the composition of ring homomorphisms.
More concisely: For any semirings R, S, and T, and ring homomorphisms f : R -> S and g : S -> T, the polynomial map operation is commutative with respect to the composition of homomorphisms: Polynomial.map (p : Poly R) (g ∘ f) = Polynomial.map (Polynomial.map p f) g.
|
Polynomial.map_monic_ne_zero
theorem Polynomial.map_monic_ne_zero :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S},
p.Monic → ∀ [inst_2 : Nontrivial S], Polynomial.map f p ≠ 0
The theorem `Polynomial.map_monic_ne_zero` states that for any polynomial `p` over a semiring `R`, if `p` is a monic polynomial (i.e., its leading coefficient is 1), then mapping `p` across any ring homomorphism `f` to another semiring `S` (where `S` is nontrivial, i.e., not equal to zero) will yield a non-zero polynomial. In other words, the action of applying a ring homomorphism to a monic polynomial does not result in the zero polynomial when the target semiring is nontrivial.
More concisely: If `p` is a monic polynomial over a semiring `R`, then the image of `p` under any nontrivial ring homomorphism `f` from `R` to another semiring `S` is a non-zero polynomial in `S`.
|
Polynomial.natDegree_map_le
theorem Polynomial.natDegree_map_le :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R),
(Polynomial.map f p).natDegree ≤ p.natDegree
The theorem `Polynomial.natDegree_map_le` states that for any semirings `R` and `S`, and for any ring homomorphism `f` from `R` to `S`, and for any polynomial `p` over `R`, the natural degree of the polynomial obtained by mapping `p` across `f` (denoted as `Polynomial.map f p`) is less than or equal to the natural degree of `p`. In other words, applying a ring homomorphism to a polynomial does not increase its natural degree.
More concisely: For any semiring homomorphism $f$ and polynomial $p$, the natural degree of $Polynomial.map\ f\ p$ is less than or equal to the natural degree of $p$.
|
Polynomial.eval_one
theorem Polynomial.eval_one : ∀ {R : Type u} [inst : Semiring R] {x : R}, Polynomial.eval x 1 = 1
The theorem `Polynomial.eval_one` states that for any type `R` equipped with a semiring structure and any element `x` of `R`, if we evaluate the polynomial `1` at `x`, we always get `1`. Essentially, this theorem underlines the fact that the constant polynomial `1` returns `1` irrespective of the value at which it is evaluated.
More concisely: For any semiring `R` and element `x` in `R`, the evaluation of the constant polynomial `1` at `x` is equal to `1`.
|
Polynomial.eval₂_hom
theorem Polynomial.eval₂_hom :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : R),
Polynomial.eval₂ f (f x) p = f (Polynomial.eval x p)
The theorem `Polynomial.eval₂_hom` states that for any semiring `R`, any semiring `S`, any polynomial `p` with coefficients in `R`, any ring homomorphism `f` from `R` to `S`, and any element `x` in `R`, the evaluation of the polynomial `p` at `f(x)` (after mapping the coefficients of `p` to `S` via `f`), is the same as first evaluating `p` at `x` in `R` and then mapping the result to `S` via `f`. In other words, the processes of evaluating a polynomial and applying a ring homomorphism commute. This is symbolically represented as `Polynomial.eval₂ f (f x) p = f (Polynomial.eval x p)`.
More concisely: For any semiring homomorphism $f$ and elements $x$ in a semiring $R$ and polynomial $p$ with coefficients in $R$, the evaluation of polynomial $p$ at $x$ and applying the homomorphism $f$ to the result are equal, that is, $f(p(x)) = p(f(x))$.
|
Polynomial.map_sum
theorem Polynomial.map_sum :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {ι : Type u_1}
(g : ι → Polynomial R) (s : Finset ι),
Polynomial.map f (s.sum fun i => g i) = s.sum fun i => Polynomial.map f (g i)
The theorem `Polynomial.map_sum` states that for any semirings `R` and `S`, ring homomorphism `f` from `R` to `S`, function `g` from an arbitrary type `ι` to a polynomial in `R`, and a finite set `s` of type `ι`, mapping the sum of the polynomials generated by `g` over the elements of `s` is the same as summing the mapped polynomials over the elements of `s`. In mathematical terms, this is equivalent to the statement that the operation of mapping a polynomial commutes with the operation of summing polynomials: \[\text{Polynomial.map}\ f \left(\sum_{i\in s} g(i)\right) = \sum_{i\in s} \text{Polynomial.map}\ f\ (g(i)).\]
More concisely: The theorem asserts that for any semirings R and S, ring homomorphism f, and function g from an arbitrary type ι to polynomials in R, the mapping of the sum of g(i) over a finite set s equals the sum of the mapped polynomials g(i) over s: Polynomial.map f (∑i∈s g i) = ∑i∈s Polynomial.map f (g i).
|
Polynomial.eval_comp
theorem Polynomial.eval_comp :
∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {x : R},
Polynomial.eval x (p.comp q) = Polynomial.eval (Polynomial.eval x q) p
The theorem `Polynomial.eval_comp` states that for any type `R` with a commutative semiring structure, and any two polynomials `p` and `q` over `R`, and for any element `x` of `R`, the evaluation of the composite of `p` and `q` at `x` is equal to the evaluation of `p` at the result of evaluating `q` at `x`. In other words, if you compose two polynomials and then evaluate the result at a point, you get the same answer as if you first evaluated the inner polynomial at that point, and then evaluated the outer polynomial at that result. This is written mathematically as $(p\circ q)(x) = p(q(x))$.
More concisely: For any commutative semiring `R`, polynomials `p` and `q` over `R`, and element `x` of `R`, $(p\circ q)(x) = p(q(x))$.
|
Polynomial.add_comp
theorem Polynomial.add_comp :
∀ {R : Type u} [inst : Semiring R] {p q r : Polynomial R}, (p + q).comp r = p.comp r + q.comp r
This theorem states that for any type `R` that forms a semiring, and for any polynomials `p`, `q`, and `r` over `R`, the composition of polynomial `r` with the sum of polynomials `p` and `q` is equal to the sum of the composition of `r` with `p` and the composition of `r` with `q`. Essentially, it establishes the distributive property of composition over addition for polynomials.
More concisely: For any semiring `R` and polynomials `p`, `q`, and `r` over `R`, the composition of `r` with the sum of `p` and `q` equals the sum of the compositions of `r` with `p` and `q`: `r * (p + q) = r * p + r * q`.
|
Polynomial.degree_map_le
theorem Polynomial.degree_map_le :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R),
(Polynomial.map f p).degree ≤ p.degree
The theorem `Polynomial.degree_map_le` states that for any semirings `R` and `S`, and for any ring homomorphism `f` from `R` to `S`, the degree of the polynomial obtained by mapping the polynomial `p` over `R` using `f` is less than or equal to the degree of the original polynomial `p`. This means that applying a ring homomorphism to a polynomial doesn't increase its degree.
More concisely: For any semirings R and S, and ring homomorphism f from R to S, the degree of the polynomial image of p under f is less than or equal to the degree of p.
|
Polynomial.eval_sub
theorem Polynomial.eval_sub :
∀ {R : Type u} [inst : Ring R] (p q : Polynomial R) (x : R),
Polynomial.eval x (p - q) = Polynomial.eval x p - Polynomial.eval x q
The theorem `Polynomial.eval_sub` states that for any ring `R`, any two polynomials `p` and `q` over `R`, and any element `x` of `R`, the value of the polynomial `p - q` evaluated at `x` is equal to the difference of the values of `p` and `q` evaluated at `x`. In other words, when we subtract one polynomial from another and then evaluate the result at a particular point, it's the same as if we evaluated each polynomial at that point and then subtracted the results. This result is a formalization of a fundamental property of polynomial arithmetic.
More concisely: For any ring `R`, polynomials `p` and `q` over `R`, and element `x` in `R`, `Polynomial.eval_sub R x (p - q) = p x - q x`.
|
Polynomial.one_comp
theorem Polynomial.one_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.comp 1 p = 1
This theorem states that for any type `R` which is a semiring and any polynomial `p` of type `R`, the composition of the polynomial `p` with the constant polynomial 1 is equal to the constant polynomial 1. In other words, it asserts that if you substitute polynomial `p` into the polynomial `1`, you get back the polynomial `1`. This theorem is a property of the composition operation on polynomials defined over a semiring.
More concisely: For any semiring `R` and polynomial `p` of type `R`, `p` composed with the constant polynomial 1 equals the constant polynomial 1. In Lean 4 notation, `(p : R → R) ∘ const 1 = const 1`.
|
Polynomial.eval₂_neg
theorem Polynomial.eval₂_neg :
∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S) {x : S},
Polynomial.eval₂ f x (-p) = -Polynomial.eval₂ f x p
This theorem, `Polynomial.eval₂_neg`, states that for any given ring `R` of type `u` and ring `S` of type `u_1`, for any polynomial `p` defined over the ring `R`, and any ring homomorphism `f` from `R` to `S`, and for any element `x` of the ring `S`, the evaluation of the negative of the polynomial `p` at `x` using `f` is equal to the negative of the evaluation of the polynomial `p` at `x` using `f`. In other words, negating the polynomial before evaluation is equivalent to negating the result of evaluation.
More concisely: For any ring homomorphism `f` and any element `x`, the evaluation of the negative of a polynomial `p` at `x` using `f` equals the negative of the evaluation of `p` at `x` using `f`.
|
Polynomial.map_comp
theorem Polynomial.map_comp :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p q : Polynomial R),
Polynomial.map f (p.comp q) = (Polynomial.map f p).comp (Polynomial.map f q)
The theorem `Polynomial.map_comp` states that for any semirings `R` and `S`, and a ring homomorphism `f` from `R` to `S`, and any polynomials `p` and `q` over `R`, the operation of mapping the composition of `p` and `q` across `f` is the same as the composition of the mappings of `p` and `q` across `f`. In mathematical terms, it asserts that for these given conditions, the operation of polynomial map commutes with the operation of polynomial composition.
More concisely: For any semirings R and S, ring homomorphism f from R to S, and polynomials p and q over R, the mapping of the composition p q across f is equal to the composition of the mappings f(p) and f(q).
|
Polynomial.map_C
theorem Polynomial.map_C :
∀ {R : Type u} {S : Type v} {a : R} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
Polynomial.map f (Polynomial.C a) = Polynomial.C (f a)
The theorem `Polynomial.map_C` states that for any semirings `R` and `S`, for any ring homomorphism `f` from `R` to `S`, and for any element `a` from `R`, the operation of mapping the constant polynomial `a` in `R` using `f` is the same as creating the constant polynomial in `S` using the image of `a` under `f`. In other words, if we map the constant polynomial `a` across the ring homomorphism `f`, we get the constant polynomial `f(a)` in the codomain.
More concisely: For any semirings R and S, and any ring homomorphism f from R to S, the constant polynomial f(a) in S is the image of the constant polynomial a in R under the mapping f.
|
Polynomial.monomial_comp
theorem Polynomial.monomial_comp :
∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} (n : ℕ),
((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
This theorem, `Polynomial.monomial_comp`, states that for any semiring `R`, any element `a` of `R`, any polynomial `p` over `R`, and any natural number `n`, the composition of the monomial `a * X^n` with `p` is equal to the constant polynomial `a` times `p` raised to the power of `n`. In essence, replacing `X` with `p` in the monomial `a * X^n` gives us `a * p^n`.
More concisely: For any semiring `R`, element `a` of `R`, polynomial `p` over `R`, and natural number `n`, `a * X^n * p = a * pow p n`.
|
Polynomial.degree_map_eq_of_leadingCoeff_ne_zero
theorem Polynomial.degree_map_eq_of_leadingCoeff_ne_zero :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
f p.leadingCoeff ≠ 0 → (Polynomial.map f p).degree = p.degree
The theorem `Polynomial.degree_map_eq_of_leadingCoeff_ne_zero` states that for any semirings `R` and `S`, a polynomial `p` over `R`, and a ring homomorphism `f` from `R` to `S`, if the leading coefficient of `p` is not mapped to zero under `f`, then the degree of the polynomial obtained by mapping all coefficients of `p` through `f` (`Polynomial.map f p`) is equal to the degree of the original polynomial `p`. In simple terms, if the highest coefficient of a polynomial is not zeroed out when a function is applied to all the coefficients, then the degree of the polynomial remains the same.
More concisely: If `f : R → S` is a ring homomorphism and the leading coefficient of polynomial `p` over semiring `R` is not mapped to zero under `f`, then the degree of `Polynomial.map f p` equals the degree of `p`.
|
Polynomial.sub_comp
theorem Polynomial.sub_comp :
∀ {R : Type u} [inst : Ring R] {p q r : Polynomial R}, (p - q).comp r = p.comp r - q.comp r
This theorem states that for any type `R` that forms a ring, and for any three polynomials `p`, `q`, and `r` over `R`, the composition of the difference of `p` and `q` with `r` equals to the difference of the compositions of `p` and `q` with `r` respectively. In mathematical terms, this can be written as `(p - q) ∘ r = p ∘ r - q ∘ r`, where `∘` denotes the composition of polynomials.
More concisely: For any rings `R` and polynomials `p`, `q`, and `r` over `R`, the composition of `p - q` with `r` equals the difference of the compositions of `p` and `q` with `r`. In other words, `(p - q) ∘ r = p ∘ r - q ∘ r`.
|
Polynomial.eval_one_map
theorem Polynomial.eval_one_map :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R),
Polynomial.eval 1 (Polynomial.map f p) = f (Polynomial.eval 1 p)
The theorem `Polynomial.eval_one_map` states that for any given semirings `R` and `S`, and for any ring homomorphism `f` from `R` to `S`, and any polynomial `p` over `R`, the value of evaluating the mapped polynomial `p` (via `f`) at 1 is equivalent to applying the ring homomorphism `f` on the value of evaluating the original polynomial `p` at 1. In other words, mapping a polynomial and then evaluating at 1 is the same as evaluating the polynomial at 1 and then applying the ring homomorphism.
More concisely: For any semirings R and S, ring homomorphism f from R to S, and polynomial p over R, the value of f(p(1)) equals p(1) \* f(1) in S.
|
Polynomial.eval_list_prod
theorem Polynomial.eval_list_prod :
∀ {R : Type u} [inst : CommSemiring R] (l : List (Polynomial R)) (x : R),
Polynomial.eval x l.prod = (List.map (Polynomial.eval x) l).prod
This theorem states that for any commutative semiring `R`, any list `l` of polynomials over `R`, and any element `x` of `R`, the evaluation at `x` of the product of the polynomials in `l` is equal to the product of the evaluations at `x` of the individual polynomials in `l`. In other words, evaluating a product of polynomials at a particular point is the same as multiplying the evaluations of the individual polynomials at that point; in mathematical terms, this can be written as `eval(x, prod(l)) = prod(map(eval(x), l))`.
More concisely: For any commutative semiring `R`, the evaluation of the product of a list of polynomials over `R` at an element `x` of `R` is equal to the product of the evaluations of the individual polynomials at `x`. In mathematical notation: `eval(x, prod(l)) = prod(map(eval(x), l))`.
|
Polynomial.eval₂_X_pow
theorem Polynomial.eval₂_X_pow :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) {n : ℕ},
Polynomial.eval₂ f x (Polynomial.X ^ n) = x ^ n
This theorem states that for any semirings `R` and `S`, given a ring homomorphism `f` from `R` to `S` and any element `x` of `S`, the evaluation of the `n`-th power of the polynomial variable (indeterminate), `Polynomial.X`, under the evaluation map `Polynomial.eval₂ f x` equals `x` to the power of `n`. In other words, when the polynomial `Polynomial.X ^ n` is evaluated at `x` using the ring homomorphism `f`, the result is the same as simply raising `x` to the power of `n`.
More concisely: For any semirings R and S, ring homomorphism f from R to S, and element x in S, the evaluation of the n-th power of the polynomial variable X under the map Polynomial.eval₂ f x equals x raised to the power of n.
|
Polynomial.eval_mul_X
theorem Polynomial.eval_mul_X :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R},
Polynomial.eval x (p * Polynomial.X) = Polynomial.eval x p * x
This theorem, named `Polynomial.eval_mul_X`, states that for any type `R` that forms a semiring and any polynomial `p` of type `R`, and any element `x` of `R`, the value of the polynomial `p` multiplied by the polynomial variable `X` evaluated at `x` is equal to the value of the polynomial `p` evaluated at `x` multiplied by `x`. In mathematical terms, this can be expressed as `eval(x, p*X) = eval(x, p) * x`, where `eval` is a function that evaluates a polynomial at a certain point, `p` is a polynomial, `X` is the polynomial variable or indeterminate, and `x` is a point in the semiring `R`.
More concisely: For any semiring `R`, polynomial `p` over `R`, and element `x` in `R`, `eval(x, p*X) = eval(x, p) * x`.
|
Polynomial.eval₂_mul_noncomm
theorem Polynomial.eval₂_mul_noncomm :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
(∀ (k : ℕ), Commute (f (q.coeff k)) x) →
Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
The theorem `Polynomial.eval₂_mul_noncomm` states that for any semirings `R` and `S`, any polynomials `p` and `q` over `R`, any ring homomorphism `f` from `R` to `S`, and an element `x` in `S`, if for every natural number `k`, the function `f` applied to the `k`-th coefficient of `q` commutes with `x`, then the polynomial evaluation function `eval₂` satisfies the property that `eval₂` of `p * q` equals `eval₂` of `p` times `eval₂` of `q`. In simpler terms, under the condition of commutativity, the function `eval₂` distributes over polynomial multiplication.
More concisely: Given semirings R and S, polynomials p and q over R, a ring homomorphism f from R to S, and an element x in S such that f(q\_(n)) = x * f(q\_(n)) for all natural numbers n, then eval₂(p * q) = eval₂(p) * eval₂(q).
|
Polynomial.map_one
theorem Polynomial.map_one :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S), Polynomial.map f 1 = 1 := by
sorry
The theorem `Polynomial.map_one` states that for any given types `R` and `S` that are semirings (i.e. they obey the properties of addition and multiplication in a ring), and any ring homomorphism `f` from `R` to `S`, the mapping of the polynomial 1 (which is a constant polynomial) under `f` is also 1. In other words, this means that applying any ring homomorphism to the constant polynomial 1 always yields the constant polynomial 1.
More concisely: For any semirings R and S and ring homomorphism f from R to S, f(1\_R) = 1\_S, where 1\_R is the multiplicative identity of R and 1\_S is the multiplicative identity of S.
|
Polynomial.eval_X
theorem Polynomial.eval_X : ∀ {R : Type u} [inst : Semiring R] {x : R}, Polynomial.eval x Polynomial.X = x
The theorem `Polynomial.eval_X` states that for any type `R` which forms a semiring (a mathematical structure which includes operations like addition and multiplication), for any element `x` from the semiring `R`, when you evaluate the polynomial 'X' (which is a monomial of degree 1, essentially making it the variable or indeterminate in the polynomial context) at the point `x`, you simply get `x` back. This reflects the basic algebraic principle that substituting a variable with a specific value in a polynomial gives you a new expression where all occurrences of the variable are replaced with that specific value.
More concisely: For any semiring `R` and element `x` in `R`, `Polynomial.eval_X x = x`.
|
Polynomial.eval₂_sub
theorem Polynomial.eval₂_sub :
∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S) {x : S},
Polynomial.eval₂ f x (p - q) = Polynomial.eval₂ f x p - Polynomial.eval₂ f x q
The theorem `Polynomial.eval₂_sub` states for any rings `R` and `S`, any homomorphism `f` from `R` to `S`, and any values `p`, `q`, and `x` where `p` and `q` are polynomials over `R` and `x` is a value in `S`, the evaluation of the difference of `p` and `q` at `x` using the homomorphism `f` is equal to the difference of the evaluations of `p` and `q` at `x` using the homomorphism `f`. In other words, we have the equality `Polynomial.eval₂ f x (p - q) = Polynomial.eval₂ f x p - Polynomial.eval₂ f x q`.
More concisely: For any homomorphism `f` between rings `R` and `S`, and polynomials `p` and `q` over `R` and value `x` in `S`, we have `Polynomial.eval₂ f x (p - q) = Polynomial.eval₂ f x p - Polynomial.eval₂ f x q`.
|
Polynomial.map_ne_zero_iff
theorem Polynomial.map_ne_zero_iff :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S},
Function.Injective ⇑f → (Polynomial.map f p ≠ 0 ↔ p ≠ 0)
The theorem `Polynomial.map_ne_zero_iff` states that, for any types `R` and `S` with `R` and `S` being semirings, any polynomial `p` of type `R`, and any ring homomorphism `f` from `R` to `S`, if the ring homomorphism `f` is injective (meaning that if `f` maps two different elements to the same element, then those two elements must have been the same), then the polynomial `p` is not the zero polynomial if and only if the polynomial obtained by mapping `p` across the ring homomorphism `f` is not the zero polynomial. In other words, a polynomial `p` is nonzero if and only if its image under an injective ring homomorphism `f` is nonzero.
More concisely: For any injective ring homomorphism between semirings `f` and polynomial `p` over ring `R`, `p` is not the zero polynomial if and only if the image of `p` under `f` is not the zero polynomial in `S`.
|
Polynomial.mul_X_comp
theorem Polynomial.mul_X_comp :
∀ {R : Type u} [inst : Semiring R] {p r : Polynomial R}, (p * Polynomial.X).comp r = p.comp r * r
The theorem `Polynomial.mul_X_comp` states that for any semiring `R` and any polynomials `p` and `r` over `R`, the composition of the polynomial `p * Polynomial.X` with `r` is equal to the composition of `p` with `r` times `r`. In other words, `(p * X) ∘ r = (p ∘ r) * r`, where `X` is the polynomial variable, `∘` denotes composition of polynomials, and `*` denotes multiplication of polynomials. The result holds regardless of the specific semiring and the specific polynomials chosen.
More concisely: For any semiring `R` and polynomials `p` and `r` over `R`, the composition of `p * X` with `r` equals the product of the compositions of `p` with `r` and `r`, where `X` is the polynomial variable, and `*` and `∘` denote multiplication and composition of polynomials, respectively.
|
Polynomial.eval_map
theorem Polynomial.eval_map :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
Polynomial.eval x (Polynomial.map f p) = Polynomial.eval₂ f x p
This theorem states that for any given semiring `R`, semiring `S`, polynomial `p` in `R`, ring homomorphism `f` from `R` to `S`, and a variable `x` in `S`, evaluating the polynomial `p` that's been mapped across `f` at `x` is identical to evaluating `p` using the ring hom `f` and variable `x`. In other words, mapping a polynomial across a ring homomorphism and then evaluating it gives the same result as directly evaluating the polynomial with the ring homomorphism and the variable.
More concisely: For any semiring homomorphism $f$ from semiring $R$ to semiring $S$, polynomial $p$ in $R$[x], and $x$ in $S$, $p^S(x) = p^R(x'\mapsto f(x))$, where $p^S$ and $p^R$ denote the polynomials $p$ evaluated in $S$ and $R$, respectively, and $x'\mapsto f(x)$ denotes the substitution of $x$ with $f(x)$ in $p$.
|
Polynomial.mem_map_rangeS
theorem Polynomial.mem_map_rangeS :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {p : Polynomial S},
p ∈ (Polynomial.mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS
This theorem states that for any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, and any polynomial `p` with coefficients from `S`, `p` belongs to the range of the semiring induced by the ring homomorphism `f` mapped over the polynomials (`RingHom.rangeS (Polynomial.mapRingHom f)`) if and only if all the coefficients of `p` (`Polynomial.coeff p n` for all natural numbers `n`) belong to the range of the semiring induced by `f` (`RingHom.rangeS f`). In other words, a polynomial is in the range of the polynomial map of a ring homomorphism if and only if its coefficients are in the range of the original ring homomorphism.
More concisely: A polynomial lies in the range of the polynomial map of a ring homomorphism if and only if all its coefficients are in the image of the homomorphism.
|
Polynomial.eval₂_eq_eval_map
theorem Polynomial.eval₂_eq_eval_map :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) {x : S},
Polynomial.eval₂ f x p = Polynomial.eval x (Polynomial.map f p)
The theorem `Polynomial.eval₂_eq_eval_map` states that for any semiring `R`, semiring `S`, polynomial `p` of type `R`, ring homomorphism `f` from `R` to `S`, and an element `x` of `S`, evaluating the polynomial `p` at `x` using `f` (`Polynomial.eval₂ f x p`) is equivalent to first mapping the polynomial `p` across `f` and then evaluating the result at `x` (`Polynomial.eval x (Polynomial.map f p)`). In other words, the process of applying the ring homomorphism to the coefficients of a polynomial and then evaluating the resulting polynomial at a particular point is the same as directly evaluating the original polynomial at the given point, taking into account the ring homomorphism.
More concisely: For any semiring homomorphism `f` from `R` to `S`, polynomial `p` over `R`, and element `x` in `S`, `Polynomial.eval₂ f x p` is equal to `Polynomial.eval x (Polynomial.map f p)`.
|
Polynomial.eval_monomial_one_add_sub
theorem Polynomial.eval_monomial_one_add_sub :
∀ {S : Type v} [inst : CommRing S] (d : ℕ) (y : S),
Polynomial.eval (1 + y) ((Polynomial.monomial d) (↑d + 1)) -
Polynomial.eval y ((Polynomial.monomial d) (↑d + 1)) =
(Finset.range (d + 1)).sum fun x_1 => ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
This theorem gives a reformulation of the binomial expansion of \((1 + y)^d\). It states that for any commutative ring \(S\) and any natural number \(d\), the difference between the evaluation of the polynomial \(1 + y\) at the monomial \(d \times (1 + y)\) and the evaluation of the polynomial \(y\) at the same monomial equals the summation from \(i = 0\) to \(d\) of the product of the binomial coefficient \({d + 1 \choose i}\), \(i\), and \(y^{i - 1}\).
More concisely: For any commutative ring S and natural number d, the value of d * (1 + y) ^ d - y ^ d is equal to the sum, from i = 0 to d, of the binomial coefficient {d + 1 cho i} * i * y^(i-1).
|
Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero
theorem Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S)
(x : S), p ∣ q → Polynomial.eval₂ f x p = 0 → Polynomial.eval₂ f x q = 0
The theorem `Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero` states that for any two polynomials `p` and `q` over a semiring `R`, a ring homomorphism `f` from `R` to a commutative semiring `S`, and an element `x` in `S`, if `p` divides `q` and evaluating `p` at `x` using the homomorphism `f` results in zero, then evaluating `q` at `x` using the same homomorphism `f` will also result in zero. In other words, if a polynomial `p` divides another polynomial `q` and `p` evaluates to zero at a certain point under a given homomorphism, then `q` must also evaluate to zero at the same point under the same homomorphism.
More concisely: If a polynomial `p` divides another polynomial `q` over a semiring and evaluating `p` at an element `x` in a commutative semiring using a ring homomorphism `f` results in zero, then evaluating `q` at `x` using the same homomorphism `f` also results in zero.
|
Polynomial.eval_eq_sum
theorem Polynomial.eval_eq_sum :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R}, Polynomial.eval x p = p.sum fun e a => a * x ^ e
This theorem, `Polynomial.eval_eq_sum`, states that for any semiring `R`, any polynomial `p` of `R`, and any element `x` of `R`, the evaluation of the polynomial `p` at `x` is equal to the sum of each term of `p`, where each term is the product of its coefficient `a` and `x` raised to the power of its exponent `e`. In other words, if you want to evaluate a polynomial at a particular point, you can do so by summing up the results of multiplying each coefficient by the value at which you are evaluating the polynomial, raised to the appropriate power. This corresponds to the standard procedure for evaluating polynomials in mathematics.
More concisely: For any semiring `R`, polynomial `p` of `R`, and `x` in `R`, `Polynomial.eval p x = sum (map (λ (a, e), a * x ^ e) p.terms)`.
|
Polynomial.eval_multiset_prod
theorem Polynomial.eval_multiset_prod :
∀ {R : Type u} [inst : CommSemiring R] (s : Multiset (Polynomial R)) (x : R),
Polynomial.eval x s.prod = (Multiset.map (Polynomial.eval x) s).prod
This theorem states that for any commutative semiring `R`, for any multiset `s` of polynomials over `R`, and for any element `x` of `R`, the action of evaluating the product of the polynomials in `s` at `x` is the same as the product of the evaluations of each polynomial in `s` at `x`. In other words, polynomial evaluation at a given point commutes with the product operation on a multiset of polynomials.
More concisely: For any commutative semiring R, given a multiset s of polynomials over R and an element x in R, the evaluation of the product of polynomials in s at x equals the product of the evaluations of each polynomial in s at x.
|
Polynomial.map_zero
theorem Polynomial.map_zero :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S), Polynomial.map f 0 = 0 := by
sorry
This theorem, `Polynomial.map_zero`, states that for any given ring homomorphism `f` from a semiring `R` to another semiring `S`, the map of the zero polynomial, under `f`, is still the zero polynomial. In mathematical terms, given a ring homomorphism `f : R → S`, we have that `f` maps the zero polynomial to the zero polynomial, i.e., `f(0) = 0`. Here, `Polynomial.map` is a function that applies a ring homomorphism to the coefficients of a polynomial.
More concisely: Given a ring homomorphism `f : R -> S`, the map of the zero polynomial under `f` is the zero polynomial, i.e., `f(0) = 0`.
|
Polynomial.C_comp
theorem Polynomial.C_comp :
∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R}, (Polynomial.C a).comp p = Polynomial.C a
This theorem states that for any semiring `R`, any element `a` of `R`, and any polynomial `p` over `R`, the composition of the constant polynomial `a` and `p` equals the constant polynomial `a`. In other words, when we substitute `p` into the constant polynomial `a`, the result is still the constant polynomial `a`. This makes sense because a constant polynomial doesn't have any variables to substitute into, so its value should remain the same no matter what polynomial we try to substitute in for its non-existent variable.
More concisely: For any semiring `R`, any element `a` in `R`, and any polynomial `p` over `R`, the constant polynomial `a` and the composition `a ∘ p` are equal.
|
Polynomial.map_mul
theorem Polynomial.map_mul :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
Polynomial.map f (p * q) = Polynomial.map f p * Polynomial.map f q
The theorem `Polynomial.map_mul` states that for any given polynomial `p` and `q` in a given semiring `R`, and a ring homomorphism `f` from `R` to another semiring `S`, the operation of mapping (applying `f`) on the product of `p` and `q` is the same as the product of the mapped polynomials `f(p)` and `f(q)`. This property is also known as the homomorphism property of ring homomorphisms in the context of multiplying polynomials.
More concisely: For any ring homomorphism between semirings and polynomials over those semirings, applying the homomorphism to the product of two polynomials is equivalent to the product of the mapped polynomials.
|
Polynomial.eval₂_C
theorem Polynomial.eval₂_C :
∀ {R : Type u} {S : Type v} {a : R} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S),
Polynomial.eval₂ f x (Polynomial.C a) = f a
This theorem states that for any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, any element `a` of `R`, and any element `x` of `S`, the evaluation of the constant polynomial `a` at `x` under the homomorphism `f` equals the image of `a` under `f`. In other words, performing a polynomial evaluation on a constant polynomial simply maps the constant through the given ring homomorphism.
More concisely: For any semirings R and S, ring homomorphism f : R -> S, element a in R, and element x in S, f(a) = (eval\_poly f a x) (constant\_poly a).
|
Polynomial.map_dvd
theorem Polynomial.map_dvd :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {x y : Polynomial R},
x ∣ y → Polynomial.map f x ∣ Polynomial.map f y
The theorem `Polynomial.map_dvd` states that for any two polynomials `x` and `y` in a semiring `R`, and a ring homomorphism `f` from `R` to another semiring `S`, if `x` divides `y` in `R`, then the map of `x` under `f` divides the map of `y` under `f` in `S`. In other words, the "divides" relation is preserved under the polynomial map induced by `f`.
More concisely: If `f` is a ring homomorphism from a semiring `R` to another semiring `S`, and `x` divides `y` in `R`, then the image of `x` under `f` divides the image of `y` under `f` in `S`.
|
Polynomial.eval₂_finset_sum
theorem Polynomial.eval₂_finset_sum :
∀ {R : Type u} {S : Type v} {ι : Type y} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (s : Finset ι)
(g : ι → Polynomial R) (x : S),
Polynomial.eval₂ f x (s.sum fun i => g i) = s.sum fun i => Polynomial.eval₂ f x (g i)
The theorem `Polynomial.eval₂_finset_sum` states that for any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, any finite set `s`, any function `g` mapping elements of `s` to polynomials in `R`, and any element `x` of `S`, the evaluation of the sum of the polynomials `g i` for `i` in `s` at `x` under the homomorphism `f` is the same as the sum of the evaluations of each polynomial `g i` at `x` under the homomorphism `f`. In mathematical notation, this theorem says that for all these elements, $\text{eval}_2 f x (\sum_{i \in s} g(i)) = \sum_{i \in s} \text{eval}_2 f x (g(i))$.
More concisely: For any semirings R and S, ring homomorphism f from R to S, finite set s, and function g mapping elements of s to polynomials in R, the evaluation of the sum of g(i) for i in s under homomorphism f is equal to the sum of the evaluations of each g(i) under f. In symbols, eval₂ f x (∑ i ∈ s g i) = ∑ i ∈ s eval₂ f x (g i).
|
Polynomial.eval₂_map
theorem Polynomial.eval₂_map :
∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S)
[inst_2 : Semiring T] (g : S →+* T) (x : T),
Polynomial.eval₂ g x (Polynomial.map f p) = Polynomial.eval₂ (g.comp f) x p
The theorem `Polynomial.eval₂_map` states that for any polynomial `p` over a semiring `R`, and ring homomorphisms `f : R → S` and `g : S → T` between semirings `R, S, T`, the evaluation of the `f`-mapped polynomial at a point `x` in `T` using `g` is equal to the evaluation of the original polynomial at `x` using the composition of the homomorphisms `g` and `f`. In more mathematical terms, it essentially states that $(g \circ f)(p(x)) = g(f(p(x)))$ for all `x` in `T`, where `$\circ$` denotes function composition.
More concisely: For any polynomial `p` over a semiring `R`, and ring homomorphisms `f : R → S` and `g : S → T`, the evaluation of `g(f(p(x)))` is equal to `p(x)` for all `x` in `T`.
|
Polynomial.map_sub
theorem Polynomial.map_sub :
∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S),
Polynomial.map f (p - q) = Polynomial.map f p - Polynomial.map f q
The theorem `Polynomial.map_sub` states that for any types `R` and `S` that are Rings, and any polynomials `p` and `q` over the ring `R`, and a ring homomorphism `f` from `R` to `S`, mapping the difference of the polynomials `p` and `q` across the ring homomorphism `f` results in the difference of the mappings of the individual polynomials. In other words, the map operation preserves subtraction in the domain of polynomials.
More concisely: For any ring homomorphism $f$ from ring $R$ to ring $S$ and polynomials $p, q$ over $R$, we have $f(p - q) = f(p) - f(q)$.
|
Polynomial.eval₂_smul
theorem Polynomial.eval₂_smul :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (g : R →+* S) (p : Polynomial R) (x : S)
{s : R}, Polynomial.eval₂ g x (s • p) = g s * Polynomial.eval₂ g x p
The theorem `Polynomial.eval₂_smul` states that for any semirings `R` and `S`, if there exists a ring homomorphism `g` from `R` to `S`, a polynomial `p` with coefficients in `R`, and an element `x` from `S`, and for any scalar `s` from `R`, the evaluation of the scaled polynomial `s • p` at `x` under the ring homomorphism `g` equals to the product of the image of `s` under `g` and the evaluation of `p` at `x` under the same ring homomorphism. In more precise terms, it asserts that `Polynomial.eval₂ g x (s • p) = g s * Polynomial.eval₂ g x p`.
More concisely: For any semirings R and S, ring homomorphism g from R to S, polynomial p with coefficients in R, and element x in S, the evaluation of the scaled polynomial s • p at x under homomorphism g equals the product of the image of s under g and the evaluation of p at x under g. That is, g(s) * Polynomial.eval₂ g x p = Polynomial.eval₂ g x (s • p).
|
Polynomial.comp_assoc
theorem Polynomial.comp_assoc :
∀ {R : Type u_1} [inst : CommSemiring R] (φ ψ χ : Polynomial R), (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
The theorem `Polynomial.comp_assoc` states that for any commutative semiring `R` and any three polynomials `φ`, `ψ`, and `χ` over `R`, the composition of the polynomials is associative. That is, composing `φ` with the result of composing `ψ` and `χ` is the same as composing the result of composing `φ` and `ψ` with `χ`. This is symbolically represented as `(φ ∘ ψ) ∘ χ = φ ∘ (ψ ∘ χ)`, where `∘` denotes the composition of polynomials.
More concisely: For any commutative semiring R and polynomials φ, ψ, and χ over R, the association of polynomial compositions holds: (φ ∘ (ψ ∘ χ)) = (ϕ ∘ ψ) ∘ χ.
|
Polynomial.eval₂_zero
theorem Polynomial.eval₂_zero :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S),
Polynomial.eval₂ f x 0 = 0
This theorem states that for any two types `R` and `S`, both equipped with a semiring structure, and a ring homomorphism `f` from `R` to `S`, and any value `x` of type `S`, evaluating the zero polynomial at `x` using ring homomorphism `f` results in zero in `S`. In other words, the evaluation of the zero polynomial under any ring homomorphism at any point is always zero.
More concisely: For any semirings R and S, ring homomorphism f from R to S, and value x in S, the evaluation of the zero polynomial through f on x equals zero in S.
|
Polynomial.eval_smul
theorem Polynomial.eval_smul :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Monoid S] [inst_2 : DistribMulAction S R]
[inst_3 : IsScalarTower S R R] (s : S) (p : Polynomial R) (x : R),
Polynomial.eval x (s • p) = s • Polynomial.eval x p
The theorem `Polynomial.eval_smul` states that for any semiring `R`, any monoid `S`, given a distributive multiplication action of `S` on `R` and a scalar tower for `S` and `R`, for any scalar `s` from `S`, any polynomial `p` over `R`, and any element `x` from `R`, the polynomial evaluation of `s` times `p` at `x` is equal to `s` times the polynomial evaluation of `p` at `x`. In other words, this theorem states that scalar multiplication commutes with polynomial evaluation.
More concisely: For any semiring R, monoid S with distributive multiaction on R, scalar tower for S and R, scalar s in S, polynomial p over R, and element x in R, we have s * (p x) = (s * p) x, where * denotes scalar multiplication and polynomial evaluation.
|
Polynomial.comp_X
theorem Polynomial.comp_X : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.comp Polynomial.X = p
This theorem, named `Polynomial.comp_X`, states that for any type `R` that is a semiring, and any polynomial `p` over `R`, the composition of `p` with the polynomial variable `X` (also known as the indeterminate) is just `p` itself. In other words, if you substitute `X` into the polynomial `p`, you get `p` back. This is similar to the mathematical notion that for any function `f(x)`, `f(x)` composed with `x` is just `f(x)`.
More concisely: For any semiring `R` and polynomial `p` over `R`, the composition of `p` with the polynomial variable `X` is equal to `p` itself.
|
Polynomial.eval_prod
theorem Polynomial.eval_prod :
∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (x : R),
Polynomial.eval x (s.prod fun j => p j) = s.prod fun j => Polynomial.eval x (p j)
The theorem `Polynomial.eval_prod` states that for any commutative semiring `R`, any finite set `s` of a certain type `ι`, any function `p` from `ι` to polynomials over `R`, and any element `x` from `R`, evaluating `x` on the product of the polynomials `p j` for each `j` in `s` is the same as the product of the evaluations of `x` on each individual polynomial `p j`. In other words, polynomial evaluation at a point `x` commutes with the operation of taking the product over a finite set of polynomials.
More concisely: For any commutative semiring R, finite set ι, function p from ι to polynomials over R, and element x in R, the evaluation of the product of polynomials p j for j in ι at x is equal to the product of the evaluations of x at each polynomial p j.
|