Polynomial.coeff_C_mul_X_pow
theorem Polynomial.coeff_C_mul_X_pow :
∀ {R : Type u} [inst : Semiring R] (x : R) (k n : ℕ),
(Polynomial.C x * Polynomial.X ^ k).coeff n = if n = k then x else 0
This theorem, named `Polynomial.coeff_C_mul_X_pow`, states that for any semiring `R`, any element `x` of `R`, and any natural numbers `k` and `n`, the coefficient of `X^n` in the polynomial formed by multiplying the constant polynomial `x` with `X` raised to the power `k` (i.e., `Polynomial.C x * Polynomial.X ^ k`) is `x` if `n` equals `k` and `0` otherwise. In other words, this polynomial has `x` as the coefficient of `X^k` and `0` as the coefficient of `X^n` for any `n` not equal to `k`.
More concisely: For any semiring `R`, the coefficient of `X^k` in the product of the constant polynomial `x` in `R` and `X^k` is `x`, while the coefficient of `X^n` for `n ≠ k` is `0`.
|
Polynomial.mul_coeff_zero
theorem Polynomial.mul_coeff_zero :
∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p * q).coeff 0 = p.coeff 0 * q.coeff 0
The theorem `Polynomial.mul_coeff_zero` states that for any semiring `R` and any two polynomials `p` and `q` over `R`, the coefficient of `X^0` in the product `p * q` is equal to the product of the `X^0` coefficients of `p` and `q` respectively. In other words, the constant term of the product of two polynomials is equal to the product of their constant terms.
More concisely: For any semirings R and polynomials p and q over R, the constant term of their product p * q is equal to the product of their constant terms.
|
Polynomial.coeff_sum
theorem Polynomial.coeff_sum :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (n : ℕ)
(f : ℕ → R → Polynomial S), (p.sum f).coeff n = p.sum fun a b => (f a b).coeff n
The theorem `Polynomial.coeff_sum` states that for any semiring `R` and `S`, given a polynomial `p` of type `Polynomial R`, a natural number `n`, and a function `f` from pairs of natural numbers and elements of `R` to `Polynomial S`, the coefficient of `X^n` in the sum of the values of the function `f` applied to the coefficients of the polynomial `p` is equal to the sum of the coefficients of `X^n` in the polynomials resulting from applying the function `f` to each pair of a power of `X` and its coefficient in `p`. In mathematical terms, this could be denoted as
```
(coeff ∘ (sum p f)) n = (sum p (λ a b, coeff (f a b) n)
```
This theorem captures a property of the way we can distribute the `coeff` function over the `sum` of polynomials.
More concisely: For any semiring `R`, `S`, polynomial `p` of type `Polynomial R`, natural number `n`, and function `f` from pairs of natural numbers and elements of `R` to `Polynomial S`, the coefficient of `X^n` in the sum of the polynomials obtained by applying `f` to each coefficient-power pair of `p` is equal to the coefficient of `X^n` in the polynomial obtained by applying `f` to each coefficient-power pair of `p` and summing the results.
|
Polynomial.coeff_C_mul
theorem Polynomial.coeff_C_mul :
∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R] (p : Polynomial R),
(Polynomial.C a * p).coeff n = a * p.coeff n
The theorem `Polynomial.coeff_C_mul` states that for any semiring `R`, any element `a` of `R`, any natural number `n`, and any polynomial `p` over `R`, the coefficient of `X^n` in the polynomial resulting from multiplying the constant polynomial `a` with `p` is equal to `a` multiplied by the coefficient of `X^n` in `p`. Essentially, when multiplying a polynomial by a constant, each coefficient of the polynomial is multiplied by that constant.
More concisely: For any semiring R, element a of R, natural number n, and polynomial p over R, the coefficient of X^n in the product of constant polynomial a and polynomial p equals a times the coefficient of X^n in p.
|
Polynomial.coeff_smul
theorem Polynomial.coeff_smul :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : SMulZeroClass S R] (r : S) (p : Polynomial R) (n : ℕ),
(r • p).coeff n = r • p.coeff n
The theorem `Polynomial.coeff_smul` states that for any given semiring `R`, smul-zero class `S`, scalar `r` of type `S`, polynomial `p` of type `Polynomial R`, and natural number `n`, the coefficient of `X^n` in the scalar multiplication of `r` and `p` is the same as the scalar multiplication of `r` and the coefficient of `X^n` in `p`. In notation, if `coeff` denotes the coefficient function and `•` denotes scalar multiplication, then `coeff (r • p) n = r • coeff p n` for all `r`, `p`, and `n` of the appropriate types.
More concisely: For any semiring R, scalar s of type S, polynomial p of type Polynomial R, and natural number n, the coefficient of X^n in the scalar multiplication of s and p is equal to the scalar multiplication of s and the coefficient of X^n in p. That is, coeff (s • p) n = s • coeff p n.
|
Polynomial.isUnit_C
theorem Polynomial.isUnit_C : ∀ {R : Type u} [inst : Semiring R] {x : R}, IsUnit (Polynomial.C x) ↔ IsUnit x
This theorem, `Polynomial.isUnit_C`, states that for any type `R` that is a semiring, and for any element `x` of type `R`, the polynomial constant `x` is a unit if and only if `x` itself is a unit. Here, a unit is an element of a monoid that has a two-sided inverse. In other words, an element `x` is a unit in the semiring `R` if and only if the polynomial constant `x` is a unit in the ring of polynomials over `R`.
More concisely: For any semiring `R` and element `x` in `R`, the polynomial constant `x` is a unit in the ring of polynomials over `R` if and only if `x` is a unit in `R`.
|
Polynomial.coeff_mul
theorem Polynomial.coeff_mul :
∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R) (n : ℕ),
(p * q).coeff n = (Finset.antidiagonal n).sum fun x => p.coeff x.1 * q.coeff x.2
The theorem `Polynomial.coeff_mul` states that for any semiring `R`, and any two polynomials `p` and `q` over `R`, the coefficient of the term of degree `n` in the product `p * q` is equal to the sum, over all pairs `(i, j)` in the antidiagonal of `n`, of the product of the coefficient of the `i`-th term of `p` and the `j`-th term of `q`. Here, the antidiagonal of `n` is the set of all pairs `(i, j)` of natural numbers such that `i + j = n`.
More concisely: For any semiring R and polynomials p and q over R, the coefficient of the term of degree n in the product p * q is the sum of the products of the coefficients of the i-th term of p and j-th term of q, over all pairs (i, j) in the antidiagonal of n.
|
Polynomial.C_mul'
theorem Polynomial.C_mul' : ∀ {R : Type u} [inst : Semiring R] (a : R) (f : Polynomial R), Polynomial.C a * f = a • f
The theorem `Polynomial.C_mul'` states that for any type `R` that is a semiring, and for any element `a` of `R` and any polynomial `f` over `R`, the result of multiplying the constant polynomial of `a` with `f` is the same as the scalar multiplication of `a` and `f`. In other words, it shows that in the context of polynomials, the constant multiplication behaves the same way as scalar multiplication.
More concisely: For any semiring `R`, element `a` in `R`, and polynomial `f` over `R`, the constant polynomial of `a` multiplied with `f` equals the scalar multiplication of `a` times `f`.
|
Polynomial.coeff_add
theorem Polynomial.coeff_add :
∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R) (n : ℕ), (p + q).coeff n = p.coeff n + q.coeff n
The theorem `Polynomial.coeff_add` states that for any semiring `R`, any polynomials `p` and `q` over `R`, and any natural number `n`, the coefficient of `X^n` in the sum of `p` and `q` is equal to the sum of the coefficients of `X^n` in `p` and in `q`. In other words, the coefficient of a given term in the sum of two polynomials is just the sum of the coefficients of that term in each of the two polynomials. This theorem corresponds to the distributive property in algebra.
More concisely: For any semiring R, polynomials p and q over R, and natural number n, the coefficient of X^n in the sum of p and q is equal to the sum of the coefficients of X^n in p and in q.
|
Polynomial.coeff_X_add_one_pow
theorem Polynomial.coeff_X_add_one_pow :
∀ (R : Type u_1) [inst : Semiring R] (n k : ℕ), ((Polynomial.X + 1) ^ n).coeff k = ↑(n.choose k)
The theorem `Polynomial.coeff_X_add_one_pow` states that for any semiring `R` and for any natural numbers `n` and `k`, the coefficient of the `k`th term in the polynomial `(X + 1)^n` is equal to the binomial coefficient "n choose k". In other words, when you expand a binomial expression `(X + 1)^n`, the coefficient of the term `X^k` is the number of ways to choose `k` items from `n` items.
More concisely: For any semiring R and natural numbers n and k, the coefficient of X^k in (X + 1)^n is equal to the binomial coefficient n choose k.
|
Polynomial.coeff_X_pow
theorem Polynomial.coeff_X_pow :
∀ {R : Type u} [inst : Semiring R] (k n : ℕ), (Polynomial.X ^ k).coeff n = if n = k then 1 else 0
The theorem `Polynomial.coeff_X_pow` states that for any semiring `R` and for any natural numbers `k` and `n`, the `n`-th coefficient of the polynomial `X^k` (where `X` is the polynomial variable) equals `1` if `n` equals `k` and `0` otherwise. Essentially, this theorem is stating that the `k`-th power of a polynomial `X` only has a non-zero coefficient at the `k`-th term, and that coefficient is `1`.
More concisely: For any semiring R and natural numbers k and n, the n-th coefficient of X^k (in the polynomial basis of X) is 1 if n = k, and 0 otherwise.
|
Polynomial.coeff_mul_C
theorem Polynomial.coeff_mul_C :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R),
(p * Polynomial.C a).coeff n = p.coeff n * a
This theorem states that for any semiring `R`, polynomial `p` in `R`, natural number `n`, and element `a` of `R`, the coefficient of `X^n` in the polynomial resulting from multiplying `p` with the constant polynomial `a` is equal to the product of the coefficient of `X^n` in `p` and `a`. In mathematical terms, if `p` is a polynomial and `a` is a constant, then the coefficient of `X^n` in `(p * a)` is `(coefficient of X^n in p) * a`.
More concisely: For any semiring `R`, polynomial `p(X)` in `R[X]`, and natural number `n`, the coefficient of `X^n` in the product `p(X) * a` is equal to the product of the coefficient of `X^n` in `p(X)` and `a`.
|
Polynomial.smul_eq_C_mul
theorem Polynomial.smul_eq_C_mul :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (a : R), a • p = Polynomial.C a * p
This theorem states that for any semiring `R`, and for any polynomial `p` and element `a` from `R`, multiplying the polynomial `p` by the scalar `a` (denoted as `a • p`) is equivalent to multiplying the polynomial `p` by the constant polynomial created from `a` (denoted as `Polynomial.C a * p`). In other words, scalar multiplication on a polynomial is the same as the multiplication by the constant polynomial of the same scalar.
More concisely: For any semiring `R`, and for all polynomials `p` in `R` and scalar `a` in `R`, the multiplication of `a` by polynomial `p` (denoted as `a • p`) is equal to the polynomial product of `p` and the constant polynomial `Polynomial.C a` (denoted as `Polynomial.C a * p`).
|
Polynomial.coeff_mul_X_pow'
theorem Polynomial.coeff_mul_X_pow' :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ),
(p * Polynomial.X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0
This theorem, named `Polynomial.coeff_mul_X_pow'`, states that for any semiring `R`, any polynomial `p` of type `Polynomial R` and any natural numbers `n` and `d`, the coefficient of `X^d` in the product of `p` and `X^n` is equal to the coefficient of `X^(d-n)` in `p` if `n` is less than or equal to `d`, and is zero otherwise. Essentially, this theorem describes the effect on the coefficients of a polynomial when it is multiplied by a power of the polynomial variable `X`.
More concisely: For any polynomial `p` and natural numbers `n` and `d`, the coefficient of `X^d` in the product `p * X^n` is equal to the coefficient of `X^(d-n)` in `p`, if `n` is less than or equal to `d`, and is zero otherwise.
|
Polynomial.coeff_X_mul
theorem Polynomial.coeff_X_mul :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (Polynomial.X * p).coeff (n + 1) = p.coeff n := by
sorry
This theorem, Polynomial.coeff_X_mul, states that for any semiring R and for any polynomial p of type R and a natural number n, the coefficient of the (n + 1)th term of the polynomial resulting from multiplying the polynomial p by the polynomial variable X, is equal to the coefficient of the nth term of the original polynomial p. In other words, multiplying a polynomial by X effectively shifts the coefficients of the polynomial one degree higher.
More concisely: For any semiring R and polynomial p of type R, the coefficient of the (n+1)th term in the product of p and X is equal to the coefficient of the nth term in p.
|
Polynomial.coeff_mul_X
theorem Polynomial.coeff_mul_X :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (p * Polynomial.X).coeff (n + 1) = p.coeff n := by
sorry
This theorem states that for any semiring `R` and for any polynomial `p` over this semiring, the coefficient of `X^(n + 1)` in the product of `p` and `X` (the polynomial variable) is the same as the coefficient of `X^n` in the polynomial `p`. In other words, multiplying a polynomial by `X` shifts all its coefficients one degree higher.
More concisely: For any semiring `R` and polynomial `p(X)` over `R`, the coefficient of `X^(n+1)` in `p(X) * X` equals the coefficient of `X^n` in `p(X)`.
|
Polynomial.finset_sum_coeff
theorem Polynomial.finset_sum_coeff :
∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) (n : ℕ),
(s.sum fun b => f b).coeff n = s.sum fun b => (f b).coeff n
The theorem `Polynomial.finset_sum_coeff` states that for any semiring `R`, any type `ι`, any finite set `s` of type `ι`, any function `f` from `ι` to `Polynomial R`, and any natural number `n`, the coefficient of `X^n` in the polynomial resulting from the sum of applying `f` to each element in `s` is equal to the sum of the coefficients of `X^n` in each polynomial obtained by applying `f` to the elements of `s`. In other words, the distribution of `f` and `Polynomial.coeff` over the sum is commutative.
More concisely: For any semiring R, type ι, finite set s of ι, function f from ι to Polynomial R, and natural number n, the coefficient of X^n in the polynomial sum of f applied to each element in s is equal to the sum of the coefficients of X^n in each polynomial obtained by applying f to the elements of s.
|
Polynomial.coeff_mul_X_pow
theorem Polynomial.coeff_mul_X_pow :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ), (p * Polynomial.X ^ n).coeff (d + n) = p.coeff d
The theorem `Polynomial.coeff_mul_X_pow` states that for any semiring `R`, given a polynomial `p` over `R`, and any natural numbers `n` and `d`, the coefficient of the term with degree `d + n` in the polynomial obtained by multiplying `p` with `X^n` (where `X` is the polynomial variable) is equal to the coefficient of the term with degree `d` in `p`. In other words, multiplying a polynomial by `X^n` simply shifts the coefficients `n` places to the right.
More concisely: For any polynomial `p` over a semiring `R` and natural numbers `d` and `n`, the coefficient of the term with degree `d+n` in `p * X^n` equals the coefficient of the term with degree `d` in `p`.
|
Polynomial.coeff_X_pow_self
theorem Polynomial.coeff_X_pow_self : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).coeff n = 1 := by
sorry
This theorem, `Polynomial.coeff_X_pow_self`, states that for any semiring `R` and for any natural number `n`, the coefficient of `X^n` in the polynomial `X^n` is 1, where `X` is the polynomial variable. In other words, if you raise the polynomial variable `X` to some power `n`, and then look at the coefficient of the `X^n` term in the resulting polynomial, that coefficient will always be 1.
More concisely: For any semiring R and natural number n, the coefficient of X^n in the polynomial X^n is 1.
|