Polynomial.coeff_erase
theorem Polynomial.coeff_erase :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n i : ℕ),
(Polynomial.erase n p).coeff i = if i = n then 0 else p.coeff i
The theorem `Polynomial.coeff_erase` states that for any semiring `R`, any polynomial `p` of type `Polynomial R`, and any natural numbers `n` and `i`, the coefficient of the term `X^i` in the polynomial resulting from erasing the `X^n` term in `p` (`Polynomial.erase n p`) is equal to zero if `i` equals `n` (since the `X^n` term has been erased), otherwise it is equal to the coefficient of the term `X^i` in the original polynomial `p`.
More concisely: For any semiring R, polynomial p of type Polynomial R, and natural numbers n and i, the coefficient of X^i in the polynomial obtained by erasing X^n from p is equal to the coefficient of X^i in p if i ≠ n, and is equal to 0 if i = n.
|
Polynomial.C_eq_zero
theorem Polynomial.C_eq_zero : ∀ {R : Type u} {a : R} [inst : Semiring R], Polynomial.C a = 0 ↔ a = 0
The theorem `Polynomial.C_eq_zero` states that for any type `R` and any element `a` of `R`, where `R` is a semiring, the constant polynomial `a` (represented as `Polynomial.C a`) is equal to the zero polynomial if and only if `a` is zero. In other words, a constant polynomial is zero if and only if its coefficient is zero.
More concisely: For any semiring R and its element a, the constant polynomial C a equals the zero polynomial if and only if a is the additive identity of R.
|
Polynomial.sum_C_mul_X_pow_eq
theorem Polynomial.sum_C_mul_X_pow_eq :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (p.sum fun n a => Polynomial.C a * Polynomial.X ^ n) = p
This theorem states that for any polynomial `p` over a semiring `R`, the sum of each of its coefficients `a` multiplied by the constant polynomial `C a` and the polynomial variable `X` raised to the power of the corresponding exponent `n`, equals the original polynomial `p`. In mathematical notation, this can be expressed as $\sum_{n} (C a) \cdot X^n = p$, where the summation ranges over all terms in the polynomial `p`.
More concisely: For any polynomial $p$ over a semiring $R$, the expression $\sum\_n (C \cdot a) \cdot X^n$ equals $p$, where $C$ is the constant associated with coefficient $a$ in $p$.
|
Polynomial.ofFinsupp_add
theorem Polynomial.ofFinsupp_add :
∀ {R : Type u} [inst : Semiring R] {a b : AddMonoidAlgebra R ℕ},
{ toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }
This theorem states that for any semiring `R` and any two elements `a` and `b` of the monoid algebra over `R` generated by the additive monoid of natural numbers (`AddMonoidAlgebra R ℕ`), the sum of the mappings `toFinsupp` from `a` and `b` into `R` is the same as the mapping `toFinsupp` from the sum of `a` and `b` into `R`. In other words, it expresses that the `toFinsupp` function, which maps from the monoid algebra to `R`, preserves the addition operation.
More concisely: For any semiring `R`, the `toFinsupp` function maps the sum of elements in the monoid algebra `AddMonoidAlgebra R ℕ` to the sum of their individual `toFinsupp` images in `R`.
|
Polynomial.ofFinsupp_single
theorem Polynomial.ofFinsupp_single :
∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R), { toFinsupp := fun₀ | n => r } = (Polynomial.monomial n) r := by
sorry
The theorem `Polynomial.ofFinsupp_single` states that for any semiring `R`, any natural number `n`, and any element `r` of `R`, the polynomial with coefficient function `fun₀ | n => r` (which assigns the value `r` to the `n`th degree and zero otherwise) is equal to the polynomial obtained by applying the monomial operator `Polynomial.monomial n` to the element `r`. This monomial operator creates a polynomial that has `r` as the coefficient of the `n`th degree term, and zero coefficients for all other degrees.
More concisely: For any semiring R and natural number n, the polynomial with degree n equal to R, and all other coefficients zero, is equal to the monomial polynomial of degree n with coefficient R.
|
Polynomial.addSubmonoid_closure_setOf_eq_monomial
theorem Polynomial.addSubmonoid_closure_setOf_eq_monomial :
∀ {R : Type u} [inst : Semiring R], AddSubmonoid.closure {p | ∃ n a, p = (Polynomial.monomial n) a} = ⊤
This theorem states that the set of all polynomials is an additive submonoid generated by monomials. More specifically, given any semiring `R`, the closure of the set of all polynomials that can be expressed as a monomial, under the operation of `AddSubmonoid.closure`, is equal to the whole set of all polynomials over the semiring `R`. In other words, any polynomial over a semiring can be written as a sum of monomials.
More concisely: Over any semiring `R`, the set of all polynomials is the additive submonoid generated by monomials in `R`.
|
Polynomial.smul_monomial
theorem Polynomial.smul_monomial :
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (a : S) (n : ℕ) (b : R),
a • (Polynomial.monomial n) b = (Polynomial.monomial n) (a • b)
This theorem, named `Polynomial.smul_monomial`, states that for any semiring `R`, any type `S` that forms a `SMulZeroClass` with `R`, any scalar `a` of type `S`, any natural number `n`, and any element `b` of `R`, the operation of scaling `b` by `a` and then constructing a monomial with exponent `n` is the same as first constructing a monomial with exponent `n` from `b` and then scaling the resulting polynomial by `a`. In other words, scalar multiplication commutes with the formation of monomials in the polynomial ring over `R`.
More concisely: For any semiring R, any type S that is a scalar multiplication zero class over R, any scalar a of type S, any natural number n, and any element b of R, the operation of scaling b by a and then forming the monomial x^n is equal to forming the monomial x^n from b and then scaling the resulting polynomial by a.
|
Polynomial.toFinsupp_smul
theorem Polynomial.toFinsupp_smul :
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (a : S) (b : Polynomial R),
(a • b).toFinsupp = a • b.toFinsupp
This theorem states that for any type `R` with a semiring structure, and any `S` that forms a scalar multiplication zero class with `R`, given any scalar `a` of type `S` and any polynomial `b` with coefficients in `R`, the operation of converting the result of scalar multiplication of `a` and `b` to a `finsupp` representation (which maps each polynomial degree to its coefficient) is equivalent to first converting `b` to a `finsupp` representation and then performing the scalar multiplication. In essence, it says that scalar multiplication commutes with the conversion to the `finsupp` representation.
More concisely: For any semiring `R`, scalar multiplication zero class `S`, scalar `a` of type `S`, and polynomial `b` with coefficients in `R`, the operation of converting `a * b` to `finsupp` is equivalent to first converting `b` to `finsupp` and then performing scalar multiplication.
|
Polynomial.toFinsupp_add
theorem Polynomial.toFinsupp_add :
∀ {R : Type u} [inst : Semiring R] (a b : Polynomial R), (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
This theorem states that for any semiring `R` and any two polynomials `a` and `b` over `R`, the 'toFinsupp' representation of the sum of `a` and `b` is equal to the sum of the 'toFinsupp' representations of `a` and `b` individually. Here, 'toFinsupp' refers to a conversion of a polynomial to a certain type of representation called a finite support function. Essentially, it's saying that converting a sum of polynomials to this representation behaves the same way as summing the individual converted polynomials.
More concisely: For any semiring `R` and polynomials `a` and `b` over `R`, the conversion of their sum to finite support representations equals the sum of the individual finite support representations.
|
Polynomial.C_mul
theorem Polynomial.C_mul :
∀ {R : Type u} {a b : R} [inst : Semiring R], Polynomial.C (a * b) = Polynomial.C a * Polynomial.C b
The theorem `Polynomial.C_mul` states that for any semiring `R` and for any elements `a` and `b` of `R`, the polynomial constant of the product of `a` and `b` is equal to the product of the polynomial constants of `a` and `b` respectively. In other words, it means that the mapping from `R` to the polynomial constants over `R` preserves multiplication. This theorem asserts the multiplicative property of constant polynomials in a semiring.
More concisely: For any semiring R and elements a and b in R, the polynomial constant of the product a * b equals the product of the polynomial constants of a and b.
|
Polynomial.C_mul_X_eq_monomial
theorem Polynomial.C_mul_X_eq_monomial :
∀ {R : Type u} {a : R} [inst : Semiring R], Polynomial.C a * Polynomial.X = (Polynomial.monomial 1) a
The theorem `Polynomial.C_mul_X_eq_monomial` states that for any semiring `R` and any element `a` of `R`, the multiplication of the constant polynomial `a` (`Polynomial.C a`) with the polynomial variable (`Polynomial.X`) results in the monomial `a * X^1` (`Polynomial.monomial 1 a`). In other words, it declares the relationship that multiplying a constant polynomial by a polynomial variable is equivalent to creating a monomial with coefficient `a` and degree 1 in the context of a semiring.
More concisely: For any semiring and element, the constant polynomial times the polynomial variable equals the monomial with coefficient the constant and degree 1.
|
Polynomial.coeff_X_one
theorem Polynomial.coeff_X_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.coeff 1 = 1
This theorem, named `Polynomial.coeff_X_one`, states that for any type `R` where `R` is a semiring, the coefficient of the term with degree 1 in the polynomial `X`, usually denoted as `X.coeff 1` or `coeff X 1`, is equal to 1. In other words, if `X` is considered as a polynomial over a semiring `R`, the coefficient of the `X^1` term in `X` is 1.
More concisely: For any semiring R, the coefficient of X^1 in the polynomial X over R is 1.
|
Polynomial.X_pow_mul_assoc_C
theorem Polynomial.X_pow_mul_assoc_C :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ} (r : R),
p * Polynomial.X ^ n * Polynomial.C r = p * Polynomial.C r * Polynomial.X ^ n
The theorem `Polynomial.X_pow_mul_assoc_C` states that for any type `R` that is a semiring, any polynomial `p` of type `R`, any natural number `n`, and any constant `r` of type `R`, the multiplication of `p`, the `n`th power of the polynomial variable `X`, and the constant polynomial `r` is equal to the multiplication of `p`, the constant polynomial `r`, and the `n`th power of `X`. In other words, this theorem shows that the multiplication operation in the context of polynomials is associative and allows the constant to be moved to the left of `X^n`.
More concisely: For any semiring `R`, polynomial `p` over `R`, natural number `n`, and constant `r` in `R`, `p * X^n = X^n * p * r`.
|
Polynomial.toFinsupp_injective
theorem Polynomial.toFinsupp_injective : ∀ {R : Type u} [inst : Semiring R], Function.Injective Polynomial.toFinsupp
The theorem `Polynomial.toFinsupp_injective` asserts that for any type `R` equipped with a semiring structure, the function `Polynomial.toFinsupp` is injective. In other words, if we have two polynomials (from the type `R`) and the `toFinsupp` function maps them to the same element of the additive monoid algebra, then those two polynomials must be the same. It is a statement about the uniqueness of the representation of polynomials in the additive monoid algebra.
More concisely: The theorem asserts that the `Polynomial.toFinsupp` function maps distinct polynomials over a semiring to distinct elements in the additive monoid algebra.
|
Polynomial.sum_zero_index
theorem Polynomial.sum_zero_index :
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (f : ℕ → R → S),
Polynomial.sum 0 f = 0
The theorem `Polynomial.sum_zero_index` states that for any type `R` with a semiring structure, any type `S` with an additive commutative monoid structure, and any function `f` from pairs of natural numbers and `R` to `S`, the sum of the values of the function `f` applied to the coefficients of the zero polynomial is equal to zero.
More concisely: For any semiring `R`, additive commutative monoid `S`, and function `f` from pairs of natural numbers and `R` to `S` representing polynomial coefficients, the sum of `f` applied to the coefficients of the zero polynomial is equal to the zero element of `S`.
|
Polynomial.coeff_update_apply
theorem Polynomial.coeff_update_apply :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R) (i : ℕ),
(p.update n a).coeff i = if i = n then a else p.coeff i
This theorem states that for any semiring `R`, any polynomial `p` over `R`, any natural number `n`, and any element `a` of `R`, the coefficient of the `i-th` term of the polynomial resulting from replacing the `n-th` coefficient of `p` with `a` is `a` if `i` is equal to `n`, otherwise, it is the `i-th` coefficient of the original polynomial `p`. In other words, only the `n-th` coefficient changes to `a` and all other coefficients remain the same.
More concisely: For any semiring `R`, polynomial `p` over `R`, natural number `n`, and element `a` of `R`, replacing the `n`-th coefficient of `p` with `a` results in a polynomial with the `i`-th coefficient equal to the original `i`-th coefficient if `i ≠ n`, and equal to `a` if `i = n`.
|
Polynomial.smul_C
theorem Polynomial.smul_C :
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (s : S) (r : R),
s • Polynomial.C r = Polynomial.C (s • r)
This theorem, `Polynomial.smul_C`, states that for any semiring `R`, and any type `S` which forms a `SMulZeroClass` with `R`, the operation of scalar multiplication `s • Polynomial.C r` (where `s` is a scalar from `S` and `r` is an element of `R`) is equivalent to `Polynomial.C (s • r)`. In other words, scalar multiplication distributes over the constant polynomial constructor `Polynomial.C`. This is a property related to the commutativity of scalar multiplication with respect to polynomial constants.
More concisely: For any semiring `R` and type `S` forming `SMulZeroClass` with `R`, the scalar multiplication of an element `s` in `S` with a constant polynomial `Polynomial.C r` in `R` is equivalent to the constant polynomial of the scalar multiplication result `s • r`.
|
Polynomial.X_ne_zero
theorem Polynomial.X_ne_zero : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R], Polynomial.X ≠ 0
This theorem states that for any type `R` with an instance of a semiring and nontriviality, the polynomial variable `X` (also known as an indeterminate) is not equal to zero. In other words, in any nontrivial semiring, the polynomial that represents a single indeterminate term (i.e., $x$ in standard algebraic notation, where $x$ is a non-zero scalar) will never be equal to zero.
More concisely: In any nontrivial semiring, the indeterminate (or polynomial variable) is non-zero.
|
Polynomial.coeff_X_zero
theorem Polynomial.coeff_X_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.coeff 0 = 0
The theorem `Polynomial.coeff_X_zero` states that, for any semiring `R`, the coefficient of the term with degree 0 in the polynomial `X` is 0. In more detailed terms, given any type `R` that forms a semiring, the operation `Polynomial.coeff Polynomial.X 0` will always return 0. This essentially says that the constant term of the polynomial `X`, which represents a polynomial variable or indeterminate, is 0.
More concisely: For any semiring `R`, the constant term (coefficient of degree 0) of the polynomial `X` over `R` is zero.
|
Polynomial.monomial_mul_monomial
theorem Polynomial.monomial_mul_monomial :
∀ {R : Type u} [inst : Semiring R] (n m : ℕ) (r s : R),
(Polynomial.monomial n) r * (Polynomial.monomial m) s = (Polynomial.monomial (n + m)) (r * s)
The theorem `Polynomial.monomial_mul_monomial` states that for any arbitrary type `R` equipped with a semiring structure, and for any two natural numbers `n` and `m` and any two elements `r` and `s` of `R`, the product of the monomial `r * X^n` and the monomial `s * X^m` equals the monomial `(r * s) * X^(n + m)`. In mathematical terms, it states that `(r * X^n) * (s * X^m) = (r * s) * X^(n + m)`. This theorem essentially describes the multiplicative behavior of monomials in a polynomial over a semiring.
More concisely: For any semiring `R` and natural numbers `n` and `m`, the product of monomials `r * X^n` and `s * X^m` equals `(r * s) * X^(n + m)`.
|
Polynomial.commute_X_pow
theorem Polynomial.commute_X_pow :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), Commute (Polynomial.X ^ n) p
This theorem states that for any semiring `R`, for any polynomial `p` of `R`, and for any natural number `n`, the `n`th power of the polynomial variable `X` commutes with `p`. In other words, `(Polynomial.X ^ n) * p = p * (Polynomial.X ^ n)`. The concept of commutativity refers to the property of certain operations, in this case multiplication, that the result is the same regardless of the order of the operands.
More concisely: For any semiring `R`, any polynomial `p` in `R[X]`, and natural number `n`, `(X^n * p) = p * (X^n)`.
|
Polynomial.ofFinsupp.injEq
theorem Polynomial.ofFinsupp.injEq :
∀ {R : Type u_1} [inst : Semiring R] (toFinsupp toFinsupp_1 : AddMonoidAlgebra R ℕ),
({ toFinsupp := toFinsupp } = { toFinsupp := toFinsupp_1 }) = (toFinsupp = toFinsupp_1)
This theorem states that for any semiring `R` and any two elements `toFinsupp` and `toFinsupp_1` of the monoid algebra generated by the additive monoid of natural numbers over `R`, the equality of the singleton sets containing `toFinsupp` and `toFinsupp_1` respectively is equivalent to the equality of `toFinsupp` and `toFinsupp_1` themselves. In other words, two sets of this form are equal if and only if their single elements are equal.
More concisely: For any semiring `R`, two elements of the monoid algebra generated by the additive monoid of natural numbers over `R` represent the same set if and only if they are equal as elements.
|
Polynomial.support_monomial
theorem Polynomial.support_monomial :
∀ {R : Type u} [inst : Semiring R] (n : ℕ) {a : R}, a ≠ 0 → ((Polynomial.monomial n) a).support = {n}
This theorem states that for any type `R` forming a semiring, any natural number `n`, and any element `a` of `R` that is not zero, the support of the monomial `a * X^n` (denoted as `Polynomial.monomial n a`) is the singleton set containing `n`. The support of a polynomial is the set of all exponents `n` for which the coefficient of `X^n` is non-zero. In other words, for a non-zero coefficient `a` and an exponent `n`, the non-zero terms of the monomial `a * X^n` only exist at the `n`th power of `X`.
More concisely: For any semiring `R`, given a non-zero element `a` in `R` and a natural number `n`, the support of the monomial `a * X^n` in the polynomial ring over `R` is the singleton set `{n}`.
|
Polynomial.toFinsupp_monomial
theorem Polynomial.toFinsupp_monomial :
∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R), ((Polynomial.monomial n) r).toFinsupp = fun₀ | n => r := by
sorry
This theorem states that for any semiring `R`, any natural number `n`, and any element `r` of `R`, the finsupp (finite support function) of the polynomial obtained by applying the monomial `r * X^n` is a function that maps `n` to `r` and all other inputs to zero. In other words, this function returns `r` when applied to `n` and `0` otherwise, which is consistent with the fact that a polynomial monomial only has one term with a non-zero coefficient.
More concisely: For any semiring `R` and natural number `n`, the finitte support function of the polynomial `r * X^n` in `R[X]` is the function mapping `i` to `(if i = n then r else 0)`.
|
Polynomial.C_injective
theorem Polynomial.C_injective : ∀ {R : Type u} [inst : Semiring R], Function.Injective ⇑Polynomial.C
The theorem `Polynomial.C_injective` states that for any type `R` with a semiring structure, the function `Polynomial.C` is injective. In other words, if `Polynomial.C` maps two elements in `R` to the same polynomial, then those two elements were originally the same. This means that distinct elements of `R` are mapped to distinct constant polynomials by `Polynomial.C`.
More concisely: For any semiring `R`, the constant polynomial map `Polynomial.C` is an injection from `R` to the polynomial ring over `R`.
|
Polynomial.X_mul_C
theorem Polynomial.X_mul_C :
∀ {R : Type u} [inst : Semiring R] (r : R), Polynomial.X * Polynomial.C r = Polynomial.C r * Polynomial.X := by
sorry
This theorem states that for any type `R` that is a semiring, and for any element `r` of `R`, the product of the polynomial variable `X` and the constant polynomial `r` is the same as the product of the constant polynomial `r` and `X`. In other words, multiplication of the polynomial variable and a constant polynomial in `R` is commutative. This theorem is a version of `Polynomial.X_mul` that avoids creating loops in the simplifier.
More concisely: For any semiring `R` and its element `r`, the polynomial multiplication of `X` and the constant polynomial `r` equals the constant polynomial multiplication of `r` and `X`.
|
Polynomial.C_0
theorem Polynomial.C_0 : ∀ {R : Type u} [inst : Semiring R], Polynomial.C 0 = 0
This theorem states that for any type `R` that has an instance of a semiring, the constant polynomial of 0 (denoted as `Polynomial.C 0`) is equal to the zero polynomial. It means that whenever we create a constant polynomial with the coefficient 0 in the semiring, we get the zero polynomial.
More concisely: For any semiring `R`, the constant polynomial `Polynomial.C 0` equals the zero polynomial.
|
Polynomial.toFinsupp_erase
theorem Polynomial.toFinsupp_erase :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
(Polynomial.erase n p).toFinsupp = Finsupp.erase n p.toFinsupp
The theorem `Polynomial.toFinsupp_erase` states that for any semiring `R`, any polynomial `p` of type `Polynomial R`, and any natural number `n`, the operation of first erasing the `X^n` term from `p` and then converting the result to a finitely supported function is equivalent to first converting `p` to a finitely supported function and then erasing the `n`-th term from it. In other words, the operations of erasing an `n`-th term and converting to a finitely supported function commute with each other.
More concisely: For any semiring `R`, given a polynomial `p` of type `Polynomial R` and a natural number `n`, the operations of erasing the `X^n` term and converting to a finitely supported function commute, i.e., `Polynomial.toFinsupp (erase X^n p) = toFinsupp p |>. erase (finset.mem_nat.val n)` (where `|>.` is Lean's infix function for right composition).
|
Polynomial.monomial_add
theorem Polynomial.monomial_add :
∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r s : R),
(Polynomial.monomial n) (r + s) = (Polynomial.monomial n) r + (Polynomial.monomial n) s
The theorem `Polynomial.monomial_add` states that for any semiring `R`, any natural number `n`, and any elements `r` and `s` of `R`, the monomial generated by the sum `(r + s)` with exponent `n` is equal to the sum of the monomials generated by `r` and `s` separately with the same exponent `n`. In other words, the operation of creating a monomial with exponent `n` distributes over the addition of elements in the semiring. This can be written symbolically as `a * X^n + b * X^n = (a + b) * X^n` where `a` and `b` are elements in the semiring `R` and `X^n` represents a monomial of degree `n`.
More concisely: For any semiring `R` and natural number `n`, the sum of monomials `(r * X^n + s * X^n)` equals `(r + s) * X^n`, where `r` and `s` are elements of `R`.
|
Polynomial.sum_monomial_index
theorem Polynomial.sum_monomial_index :
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] {n : ℕ} (a : R) (f : ℕ → R → S),
f n 0 = 0 → ((Polynomial.monomial n) a).sum f = f n a
This theorem states that for any semiring `R`, any additive commutative monoid `S`, any natural number `n`, any element `a` of `R`, and any function `f` from pairs of natural numbers and elements of `R` to elements of `S` (where `f(n, 0)` is defined to be `0`), the sum of the function `f` applied to the coefficients of the polynomial that is equal to the monomial `a * X^n` is equal to `f(n, a)`. In simpler terms, when we apply the function `f` to each coefficient of the monomial `a * X^n` and sum the results, we get `f(n, a)`.
More concisely: For any semiring `R`, additive commutative monoid `S`, natural number `n`, `R` element `a`, and function `f` from pairs of natural numbers and `R` to `S` (with `f(n, 0) = 0`), we have the sum of `f(i, a)` for `i` from `0` to `n` equals `f(n, a)`.
|
Polynomial.not_mem_support_iff
theorem Polynomial.not_mem_support_iff :
∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, n ∉ p.support ↔ p.coeff n = 0
The theorem `Polynomial.not_mem_support_iff` states that for any type `R` under a Semiring structure, any natural number `n`, and any polynomial `p` of type `R`, the natural number `n` is not in the support of the polynomial `p` if and only if the coefficient of `X^n` in `p` is zero. Here, the "support" of the polynomial `p` is defined as the set of all `n` for which the coefficient of `X^n` is non-zero.
More concisely: For any semiring R, polynomial p of R in X, and natural number n, n is not in the support of p if and only if the coefficient of X^n in p is zero.
|
Polynomial.coeff_zero
theorem Polynomial.coeff_zero : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), Polynomial.coeff 0 n = 0
This theorem states that for any semiring `R` and natural number `n`, the coefficient of `X^n` in the zero polynomial (which is a polynomial with all coefficients equal to zero) is zero. In more mathematical terms, if `p(X)` represents the zero polynomial in `R[X]`, the theorem says that the coefficient of `X^n` in `p(X)` is zero for any `n ∈ ℕ`.
More concisely: For any semiring `R` and natural number `n`, the coefficient of `X^n` in the zero polynomial `p(X)` over `R` is equal to zero.
|
Polynomial.coeff_monomial
theorem Polynomial.coeff_monomial :
∀ {R : Type u} {a : R} {m n : ℕ} [inst : Semiring R],
((Polynomial.monomial n) a).coeff m = if n = m then a else 0
The theorem `Polynomial.coeff_monomial` states that for any type `R`, an element `a` of `R`, and natural numbers `m` and `n`, given a semiring structure on `R`, the coefficient of the polynomial obtained by applying the `Polynomial.monomial` function on `n` and `a` at the index `m` is `a` if `n` is equal to `m`, and `0` otherwise. In other words, in the monomial `a * X^n`, the coefficient of `X^m` is `a` if `m` equals `n`, and `0` if `m` does not equal `n`.
More concisely: For any semiring `R`, `n`, `m` in `ℕ`, and `a` in `R`, the coefficient of the monomial `a * X^n` in the polynomial `Polynomial.monomial R a X n` is `a` if `n = m`, and `0` otherwise.
|
Polynomial.coeff_neg
theorem Polynomial.coeff_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (n : ℕ), (-p).coeff n = -p.coeff n
This theorem, `Polynomial.coeff_neg`, states that for any given type `R` that is a ring, for any polynomial `p` of type `R` and for any natural number `n`, the coefficient of `X^n` in the negation of `p` (`-p`) is equal to the negation of the coefficient of `X^n` in `p`. In other words, negating a polynomial negates each of its coefficients.
More concisely: For any ring type R, polynomial p of type R, and natural number n, the coefficient of X^n in the negation of p is the negation of the coefficient of X^n in p.
|
Polynomial.sum_C_index
theorem Polynomial.sum_C_index :
∀ {R : Type u} [inst : Semiring R] {a : R} {β : Type u_1} [inst_1 : AddCommMonoid β] {f : ℕ → R → β},
f 0 0 = 0 → (Polynomial.C a).sum f = f 0 a
The theorem `Polynomial.sum_C_index` states that for any semiring `R`, any element `a` of `R`, any type `β` that is an additive commutative monoid, and any function `f` from `ℕ` x `R` to `β`, if `f` maps `(0, 0)` to `0`, then the sum of the values of `f` applied to the coefficients of the constant polynomial `a` is equal to `f` applied to `(0, a)`. In simpler terms, this means that the sum of the function `f` applied to the coefficients of a constant polynomial only depends on the zeroth coefficient.
More concisely: For any semiring `R`, any additive commutative monoid `β`, any function `f` from `ℕ x R` to `β` that maps `(0, 0)` to `0`, the sum of `f` applied to the coefficients of a constant polynomial equals `f` applied to `(0, coefficient of constant polynomial)`.
|
Polynomial.C_inj
theorem Polynomial.C_inj : ∀ {R : Type u} {a b : R} [inst : Semiring R], Polynomial.C a = Polynomial.C b ↔ a = b := by
sorry
The theorem `Polynomial.C_inj` states that for any type `R` that has a structure of semiring, and for any two elements `a` and `b` of `R`, the constant polynomial determined by `a` is equal to the constant polynomial determined by `b` if and only if `a` is equal to `b`. In other words, the map that associates to each element of the ring its corresponding constant polynomial is injective.
More concisely: The map from a semiring to its constant polynomials is an injection.
|
Polynomial.X_pow_eq_monomial
theorem Polynomial.X_pow_eq_monomial :
∀ {R : Type u} [inst : Semiring R] (n : ℕ), Polynomial.X ^ n = (Polynomial.monomial n) 1
This theorem states that for any semiring `R` and for any natural number `n`, the `n`-th power of the polynomial variable `X` is equal to the monomial `1 * X^n`. In other words, raising the polynomial variable `X` to the power of `n` creates a monomial where the coefficient is `1` and the exponent is `n`. This is valid in the context of any semiring, a mathematical structure that includes operations of addition and multiplication.
More concisely: For any semiring `R` and natural number `n`, the `n`-th power of the polynomial variable `X` equals the monomial `1 * X^n`.
|
Polynomial.C_1
theorem Polynomial.C_1 : ∀ {R : Type u} [inst : Semiring R], Polynomial.C 1 = 1
The theorem `Polynomial.C_1` states that for all semirings `R`, the constant polynomial of `1` is `1`. In other words, when we apply the constant polynomial constructor `Polynomial.C` to the multiplicative identity `1` in any semiring `R`, we obtain the multiplicative identity in the ring of polynomials over `R`. This is a property of the constant polynomial mapping in the context of ring theory.
More concisely: For any semiring R, the constant polynomial over the multiplicative identity 1 in R is equal to the multiplicative identity in the ring of polynomials over R.
|
Polynomial.erase_def
theorem Polynomial.erase_def :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (x : Polynomial R),
Polynomial.erase n x =
match x with
| { toFinsupp := p } => { toFinsupp := Finsupp.erase n p }
This theorem is about the erasure of a term in a polynomial. Specifically, for any semiring `R`, natural number `n`, and polynomial `x` over `R`, the function `Polynomial.erase n x` is equal to the polynomial derived by erasing the `n`th term from the finitely supported function representation of `x`. In other words, the erasure of the `X^n` term in the polynomial `x` produces a new polynomial which is identical to `x` except that the coefficient of `X^n` is now zero.
More concisely: For any semiring `R`, natural number `n`, and polynomial `x` over `R`, the polynomial `Polynomial.erase n x` equals `x` with the coefficient of `X^n` replaced by zero.
|
Polynomial.C_add
theorem Polynomial.C_add :
∀ {R : Type u} {a b : R} [inst : Semiring R], Polynomial.C (a + b) = Polynomial.C a + Polynomial.C b
The theorem `Polynomial.C_add` states that for any type `R`, and any elements `a` and `b` of `R` where `R` is a semiring, the constant polynomial of the sum of `a` and `b` (`Polynomial.C (a + b)`) is equal to the sum of the constant polynomials of `a` and `b` (`Polynomial.C a + Polynomial.C b`). In other words, it states that the constant polynomial function preserves addition in the underlying semiring `R`.
More concisely: For any semiring R and elements a, b in R, Polynomial.C (a + b) = Polynomial.C a + Polynomial.C b.
|
Polynomial.card_support_eq_zero
theorem Polynomial.card_support_eq_zero :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.card = 0 ↔ p = 0
This theorem states that for any semiring `R` and any polynomial `p` over `R`, the cardinality (i.e., the number of elements) of the support of `p` is zero if and only if `p` is the zero polynomial. Here, the support of a polynomial `p` is defined as the set of all `n` such that the `n`-th power of `X` has a non-zero coefficient in `p`.
More concisely: For any semiring `R` and polynomial `p` over `R`, the polynomial `p` is the zero polynomial if and only if the cardinality of the support of `p` is zero.
|
Polynomial.sum_monomial_eq
theorem Polynomial.sum_monomial_eq :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (p.sum fun n a => (Polynomial.monomial n) a) = p
The theorem `Polynomial.sum_monomial_eq` states that for any polynomial `p` over a semiring `R`, if we sum the values of the function that applies the coefficients of the polynomial `p` to the monomial function `Polynomial.monomial`, we get back the original polynomial `p`. In other words, the sum of the monomials of the polynomial, each multiplied by its corresponding coefficient, reconstitutes the original polynomial. This is analogous to expressing a polynomial as the sum of its monomial terms.
More concisely: For any polynomial `p` over a semiring `R`, the sum of the products of its coefficients with the monomial functions is equal to `p`.
|
Polynomial.support_monomial'
theorem Polynomial.support_monomial' :
∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), ((Polynomial.monomial n) a).support ⊆ {n}
The theorem `Polynomial.support_monomial'` states that for any semiring `R`, any natural number `n`, and any element `a` of `R`, the support of the monomial `a * X^n` (where `X` is an indeterminate) is a subset of the singleton set containing `n`. The support of a polynomial is the set of all powers `n` such that `X^n` has a non-zero coefficient. In simpler terms, this theorem says that the only power of `X` that may have a non-zero coefficient in the monomial `a * X^n` is `n`.
More concisely: For any semiring R, natural number n, and element a in R, the support of the monomial a * X^n contains only the power n.
|
Polynomial.ext
theorem Polynomial.ext :
∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q
The theorem `Polynomial.ext` asserts that for any type `R` that is a semiring and any two polynomials `p` and `q` over this semiring, if the coefficient of `X^n` in `p` is equal to the coefficient of `X^n` in `q` for every natural number `n`, then the polynomials `p` and `q` are identical. In other words, two polynomials are the same if and only if they have the same coefficients for each degree in the natural numbers.
More concisely: Given semirings R and polynomials p and q over R, if for all natural numbers n, the coefficients of X^n in p and q are equal, then p and q are identical.
|
Polynomial.monomial_mul_X
theorem Polynomial.monomial_mul_X :
∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R),
(Polynomial.monomial n) r * Polynomial.X = (Polynomial.monomial (n + 1)) r
The theorem `Polynomial.monomial_mul_X` states that for any semiring `R`, any natural number `n`, and any element `r` of `R`, the product of the monomial `r * X^n` with the polynomial variable `X` is equal to the monomial `r * X^(n+1)`. In other words, multiplying a monomial by `X` simply increments the exponent of `X` in that monomial by 1, without changing the coefficient.
More concisely: For any semiring R, natural number n, and element r of R, the product of the monomial r * X^n with the polynomial variable X is equal to the monomial r * X^(n+1).
|
Polynomial.coeff_one_zero
theorem Polynomial.coeff_one_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.coeff 1 0 = 1
The theorem `Polynomial.coeff_one_zero` states that for any semiring `R`, the coefficient of `X^0` in the polynomial `1` is `1`. In other words, when you look at the constant polynomial `1` and retrieve the coefficient of the term `X^0`, you will always get `1`.
More concisely: For any semiring R, the constant polynomial 1 in R[X] has a coefficient of 1 for the term X^0.
|
Polynomial.ofFinsupp_inj
theorem Polynomial.ofFinsupp_inj :
∀ {R : Type u} [inst : Semiring R] {a b : AddMonoidAlgebra R ℕ}, { toFinsupp := a } = { toFinsupp := b } ↔ a = b
This theorem states that for all types `R` which is a semiring and any two additive monoid algebras `a` and `b` over `R` and `ℕ` respectively, the equality of the polynomial formed from `a` and the polynomial formed from `b` (represented by their corresponding `toFinsupp` mappings) is equivalent to the equality of `a` and `b` themselves. Therefore, it provides a more convenient way to assert the equality of two polynomials using their additive monoid algebra representations.
More concisely: For any semiring R and additive monoid algebras a and b over R and ℕ respectively, the equality of their corresponding toFinsupp polynomials implies the equality of a and b.
|
Polynomial.support_ofFinsupp
theorem Polynomial.support_ofFinsupp :
∀ {R : Type u} [inst : Semiring R] (p : AddMonoidAlgebra R ℕ), { toFinsupp := p }.support = p.support
This theorem states that for any semiring `R` and any polynomial `p` represented as an additive monoid algebra over `R`, the set of powers of `X` (i.e., `n`) with non-zero coefficients in the polynomial is exactly the same as the support of the monoid algebra `p`. In other words, the positions where the polynomial has non-zero coefficients correspond exactly to the elements of the additive monoid that are present in the monoid algebra.
More concisely: For any semiring `R` and polynomial `p` over `R`, the set of exponents of non-zero coefficients in `p` is equal to the support of the additive monoid algebra generated by `p` over `R`.
|
Polynomial.support_C_mul_X_pow'
theorem Polynomial.support_C_mul_X_pow' :
∀ {R : Type u} [inst : Semiring R] (n : ℕ) (c : R), (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
The theorem `Polynomial.support_C_mul_X_pow'` states that for any semiring `R`, any natural number `n`, and any element `c` of `R`, the support of the polynomial, which is the product of the constant polynomial `c` and `X` raised to the power `n`, is a subset of the singleton set that contains only `n`. In practical terms, this means that the only exponent of `X` that can have a non-zero coefficient in the polynomial `c * X^n` is `n` itself.
More concisely: The theorem asserts that the support of the polynomial `c * X^n` in a semiring consists only of the exponent `n` for any natural number `n` and element `c` in the semiring.
|
Polynomial.sum_add_index
theorem Polynomial.sum_add_index :
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p q : Polynomial R) (f : ℕ → R → S),
(∀ (i : ℕ), f i 0 = 0) →
(∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂) → (p + q).sum f = p.sum f + q.sum f
The theorem `Polynomial.sum_add_index` states that for any two polynomials `p` and `q` over a semiring `R`, and any function `f` from pairs of natural numbers and elements of `R` to a type `S` with an additive commutative monoid structure, if `f` maps any pair consisting of a natural number and the zero element of `R` to the zero element of `S`, and `f` distributes over addition in `R` (i.e., for any natural number `a` and elements `b₁`, `b₂` of `R`, `f` of `a` and the sum of `b₁` and `b₂` is equal to the sum of `f` of `a` and `b₁` and `f` of `a` and `b₂`), then the sum of the values of `f` applied to the coefficients of the sum of `p` and `q` is equal to the sum of the sum of the values of `f` applied to the coefficients of `p` and the sum of the values of `f` applied to the coefficients of `q`. In other words, the operation of summing the values of `f` applied to the coefficients of a polynomial is compatible with the addition of polynomials.
More concisely: Given polynomials `p` and `q` over a semiring `R`, and a function `f` from pairs of natural numbers and elements of `R` to an additive commutative monoid `S` such that `f` maps any pair consisting of a natural number and the zero element of `R` to the zero element of `S` and distributes over addition in `R`, the sum of the values of `f` applied to the coefficients of `p + q` equals the sum of the values of `f` applied to the coefficients of `p` and the coefficients of `q`.
|
Polynomial.commute_X
theorem Polynomial.commute_X : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), Commute Polynomial.X p
This theorem states that for any type `R` that forms a semiring, and for any polynomial `p` with coefficients from `R`, the polynomial variable `X` commutes with `p`. In other words, the order in which `X` and `p` are multiplied does not affect the result; mathematically, this means `X * p = p * X` for all polynomials `p` in the semiring `R`.
More concisely: For any semiring `R` and polynomial `p` with coefficients from `R`, the commutativity of multiplication holds between `X` and `p`, that is, `X * p = p * X`.
|
Polynomial.coeff_C_succ
theorem Polynomial.coeff_C_succ :
∀ {R : Type u} [inst : Semiring R] {r : R} {n : ℕ}, (Polynomial.C r).coeff (n + 1) = 0
The theorem `Polynomial.coeff_C_succ` states that for any semiring `R`, any element `r` of `R`, and any natural number `n`, the coefficient of the term `X^(n+1)` in the constant polynomial `r` is `0`. In other words, it confirms that the constant polynomial `r` in the semiring `R` does not have any terms of degree greater than `0`, by ensuring that all coefficients of higher degree terms are `0`.
More concisely: The theorem `Polynomial.coeff_C_succ` asserts that the coefficient of the term `X^(n+1)` in the constant polynomial `r` over a semiring `R` is equal to `0` for any natural number `n`.
|
Polynomial.ext_iff
theorem Polynomial.ext_iff :
∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
This theorem states that for any semiring R, two polynomials p and q (of type R) are equal if and only if their coefficients for every natural number n are equal. In other words, two polynomials are identical exactly when they have the same coefficients for the power of `X` in each term.
More concisely: For any semiring R, two polynomials p and q over R are equal if and only if their corresponding coefficients are equal for all natural numbers n.
|
Polynomial.toFinsupp_mul
theorem Polynomial.toFinsupp_mul :
∀ {R : Type u} [inst : Semiring R] (a b : Polynomial R), (a * b).toFinsupp = a.toFinsupp * b.toFinsupp
This theorem states that for any given semiring `R` and any two polynomials `a` and `b` over `R`, the polynomial obtained by multiplying `a` and `b` and then converting to a `Finsupp` representation is equal to the `Finsupp` representation of `a` multiplied by the `Finsupp` representation of `b`. Here, `Finsupp` is a type of sparse representation of functions.
More concisely: For any semiring `R` and polynomials `a` and `b` over `R`, the `Finsupp` representation of their product equals the product of their individual `Finsupp` representations.
|
Polynomial.sum_def
theorem Polynomial.sum_def :
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S),
p.sum f = p.support.sum fun n => f n (p.coeff n)
The theorem `Polynomial.sum_def` states that for any semiring `R`, additively commutative monoid `S`, polynomial `p` over `R`, and function `f` from a pair of natural number and `R` to `S`, the sum obtained by applying `f` to each coefficient of the polynomial `p` is equal to the sum of `f` applied to each element `n` and its corresponding coefficient in the polynomial, where `n` ranges over the support of the polynomial `p`. Here, the support of a polynomial is the set of all exponents such that the corresponding coefficient is non-zero.
More concisely: For any semiring `R`, additively commutative monoid `S`, polynomial `p` over `R` with support `N`, and function `f : ℕ × R → S`, the application of `f` to the coefficient-wise sum of the polynomial `p` is equal to the sum of `f(n, p(n))` for all `n` in the support `N` of `p`.
|
Polynomial.coeff_C
theorem Polynomial.coeff_C :
∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], (Polynomial.C a).coeff n = if n = 0 then a else 0
The theorem `Polynomial.coeff_C` states that for any type `R` which is a semiring, any element `a` of `R`, and any natural number `n`, the coefficient of `X^n` in the constant polynomial `a` is `a` if `n` is 0 and 0 otherwise. In other words, the only nonzero coefficient of a constant polynomial is the constant itself, which is the coefficient of `X^0`.
More concisely: For any semiring `R` and element `a` in `R`, the coefficient of `X^0` in the polynomial `a` is `a`, while the coefficients of all other powers of `X` are `0`.
|
Polynomial.support_erase
theorem Polynomial.support_erase :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (Polynomial.erase n p).support = p.support.erase n
This theorem states that for any semiring `R`, any polynomial `p` from `R`, and any natural number `n`, the support (i.e., the set of all powers `n` for which the `X^n` term of the polynomial has a non-zero coefficient) of the polynomial obtained by erasing the `X^n` term from `p` is equal to the set obtained by erasing `n` from the support of `p`. In other words, removing the `X^n` term from a polynomial precisely removes `n` from the set of powers with non-zero coefficients in the polynomial.
More concisely: For any semiring `R`, polynomial `p` from `R` in the indeterminate `X`, and natural number `n`, the support of the polynomial `p` without the `X^n` term equals the support of `p` without `n`.
|
Polynomial.C_neg
theorem Polynomial.C_neg : ∀ {R : Type u} {a : R} [inst : Ring R], Polynomial.C (-a) = -Polynomial.C a
The theorem `Polynomial.C_neg` states that for any type `R` and any element `a` of `R`, where `R` is a ring, the constant polynomial of `-a` is equivalent to the negation of the constant polynomial of `a`. In other words, if we denote the constant polynomial associated with a value as `Polynomial.C`, then `Polynomial.C` maps negation in the ring to negation in the ring of polynomials. This can be expressed mathematically as: for all `a` in ring `R`, `Polynomial.C(-a) = -Polynomial.C(a)`.
More concisely: For any ring `R` and its element `a`, the constant polynomial of `-a` equals the negation of the constant polynomial of `a`: `Polynomial.C(-a) = -Polynomial.C(a)`.
|
Polynomial.mem_support_iff
theorem Polynomial.mem_support_iff :
∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, n ∈ p.support ↔ p.coeff n ≠ 0
The theorem `Polynomial.mem_support_iff` states that for any given type `R` (which is a semiring), a natural number `n`, and a polynomial `p` of type `R`, the number `n` is in the support of the polynomial `p` if and only if the coefficient of `X^n` in `p` is non-zero. This support of a polynomial is defined as the set of all `n` such that `X^n` has a non-zero coefficient. Hence, this theorem is connecting the concept of the support of a polynomial to the non-zero coefficients of the polynomial.
More concisely: For any semiring R, natural number n, and polynomial p over R, n is in the support of p if and only if the coefficient of X^n in p is non-zero.
|
Polynomial.C_mul_X_pow_eq_monomial
theorem Polynomial.C_mul_X_pow_eq_monomial :
∀ {R : Type u} {a : R} [inst : Semiring R] {n : ℕ}, Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
This theorem establishes a correspondence between the multiplication of a constant polynomial and a power of the polynomial variable, and a monomial, in the context of semirings. Specifically, it states that for any semiring `R`, given a constant `a` from `R` and a natural number `n`, the multiplication of the constant polynomial `a` and the `n`-th power of the polynomial variable is equivalent to the monomial constituted by `a` and `n`. This effectively means that `Polynomial.C a * Polynomial.X ^ n` gives the same polynomial as `(Polynomial.monomial n) a` does.
More concisely: For any semiring `R` and constant `a` from `R` and natural number `n`, the product of the constant polynomial `a` and the `n`-th power of the polynomial variable is equal to the monomial `(a :: R) * X ^ n`.
|
Polynomial.support_eq_empty
theorem Polynomial.support_eq_empty : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support = ∅ ↔ p = 0 := by
sorry
This theorem states that for any type `R` which forms a semiring, and for any polynomial `p` with coefficients in `R`, the support of the polynomial `p` (that is, the set of all exponents `n` such that `X^n` has a non-zero coefficient in the polynomial) is empty if and only if the polynomial `p` is the zero polynomial. In other words, a polynomial has no non-zero coefficients if and only if it is the zero polynomial.
More concisely: A polynomial over a semiring has an empty support if and only if it is the zero polynomial.
|
Polynomial.monomial_zero_right
theorem Polynomial.monomial_zero_right : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.monomial n) 0 = 0 := by
sorry
The theorem `Polynomial.monomial_zero_right` states that for all natural numbers `n` and for any type `R` in the context of a semiring, the monomial generated by the function `Polynomial.monomial` when applied to `n` and 0 is equal to 0. In other words, when multiplying 0 by any power of a variable `X`, the result will always be 0.
More concisely: For all natural numbers `n` and in any semiring `R`, the monomial generated by the function `Polynomial.monomial` from `R` with variables `X` and coefficient `n`, applied to `X` and `0`, equals `0`.
|
Polynomial.X_pow_mul_C
theorem Polynomial.X_pow_mul_C :
∀ {R : Type u} [inst : Semiring R] (r : R) (n : ℕ),
Polynomial.X ^ n * Polynomial.C r = Polynomial.C r * Polynomial.X ^ n
This theorem, `Polynomial.X_pow_mul_C`, states that for any semiring `R`, any element `r` of `R`, and any natural number `n`, the polynomial represented by the variable `X` raised to the power `n`, multiplied by the constant polynomial `r` is equal to the constant polynomial `r` multiplied by the variable `X` raised to the power `n`. In other words, the multiplication of a variable polynomial and a constant polynomial is commutative, even when the variable polynomial is raised to a power. It is a helper theorem used to simplify expressions in polynomial algebra, specifically to ensure that constants are placed to the left of the variable polynomial in multiplication expressions.
More concisely: For any semiring `R`, any element `r` of `R`, and natural number `n`, the polynomial `X^n * r` equals `r * X^n`.
|
Polynomial.X_pow_mul
theorem Polynomial.X_pow_mul :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, Polynomial.X ^ n * p = p * Polynomial.X ^ n := by
sorry
The theorem `Polynomial.X_pow_mul` states that for any type `R` that is a semiring, any polynomial `p` of type `R`, and any natural number `n`, the product of `Polynomial.X` raised to the power `n` and `p` is equal to the product of `p` and `Polynomial.X` raised to the power `n`. In simple terms, this theorem asserts the commutativity of multiplication between a power of the polynomial variable `Polynomial.X` and any other polynomial in a semiring.
More concisely: For any semiring `R`, any polynomial `p` over `R`, and any natural number `n`, the power `p` of the indeterminate `X` in the polynomial ring `Polynomial R` commutes with multiplication by `p`, i.e., `X^n * p = p * X^n`.
|
Polynomial.coeff_one
theorem Polynomial.coeff_one :
∀ {R : Type u} [inst : Semiring R] {n : ℕ}, Polynomial.coeff 1 n = if n = 0 then 1 else 0
The theorem `Polynomial.coeff_one` states that for any semiring `R` and any natural number `n`, the coefficient of `X^n` in a polynomial equal to 1 is 1 if `n` equals 0, and is 0 otherwise. In other words, it says that a constant polynomial of 1 only has a non-zero coefficient for `X^0` (the constant term), and all other coefficients are zero.
More concisely: For any semiring R and natural number n, the coefficient of X^n in the polynomial equal to 1 is 1 if n = 0, and 0 otherwise.
|
Polynomial.ofFinsupp_neg
theorem Polynomial.ofFinsupp_neg :
∀ {R : Type u} [inst : Ring R] {a : AddMonoidAlgebra R ℕ}, { toFinsupp := -a } = -{ toFinsupp := a }
This theorem states that for any ring `R` and an additive monoid algebra `a` over `R` and the natural numbers, the negative of the Finsupp conversion of `a` equals the Finsupp conversion of the negative of `a`. In other words, the operation of negation commutes with the Finsupp conversion in the context of additive monoid algebras over a ring and the natural numbers. The Finsupp conversion is a method to represent elements of the additive monoid algebra as formal finite linear combinations.
More concisely: For any additive monoid algebra `a` over a ring `R` and the natural numbers, the negation of its Finsupp conversion is equal to the Finsupp conversion of the negation of `a`.
|
Polynomial.X_mul
theorem Polynomial.X_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.X * p = p * Polynomial.X
The theorem `Polynomial.X_mul` states that, for any semiring `R`, and any polynomial `p` with coefficients in `R`, the polynomial variable `X` commutes with `p`. In other words, multiplying `X` by `p` is the same as multiplying `p` by `X`. This is true even when the coefficients in `R` are noncommutative. In mathematical terms, if we denote by `X` the polynomial variable and `p` is any polynomial, then `X * p = p * X`.
More concisely: For any semiring `R` and polynomial `p` over `R`, `X * p = p * X`, where `X` is a polynomial variable.
|
Polynomial.mul_eq_sum_sum
theorem Polynomial.mul_eq_sum_sum :
∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
p * q = p.support.sum fun i => q.sum fun j a => (Polynomial.monomial (i + j)) (p.coeff i * a)
This theorem states that, for any given semiring `R` and any two polynomials `p` and `q` over that semiring, the product of `p` and `q` is equal to the double sum over the support of `p` and `q`. Specifically, for each pair of indices `(i, j)`, we multiply the `i`-th coefficient of `p` with the `j`-th coefficient of `q`, and then form a monomial with this product as the coefficient and `i + j` as the exponent. Summing these monomials over all `(i, j)` gives the product of the two polynomials. This reflects the standard procedure for multiplying two polynomials: each term in the first polynomial is multiplied with each term in the second polynomial, and the resulting terms are summed together.
More concisely: For any semiring `R` and polynomials `p` and `q` over `R`, their product equals the double sum over the support of `p` and `q` where the `(i, j)`-th term is the product of the `i`-th coefficient of `p` and the `j`-th coefficient of `q`, with exponent `i + j`.
|
Polynomial.coeff_C_zero
theorem Polynomial.coeff_C_zero : ∀ {R : Type u} {a : R} [inst : Semiring R], (Polynomial.C a).coeff 0 = a
The theorem `Polynomial.coeff_C_zero` states that for any arbitrary type `R` and any element `a` of type `R`, given that `R` is a semiring, the coefficient of the constant polynomial `a` at degree 0 is `a`. In other words, if you have a constant polynomial whose only term is `a*X^0` (which simplifies to `a` as anything raised to the power of 0 is 1), then the coefficient for the `X^0` term (i.e., the term with degree 0) is `a`.
More concisely: For any semiring `R` and its element `a`, the constant polynomial `a` has coefficient `a` at degree 0.
|
Polynomial.coeff_sub
theorem Polynomial.coeff_sub :
∀ {R : Type u} [inst : Ring R] (p q : Polynomial R) (n : ℕ), (p - q).coeff n = p.coeff n - q.coeff n
The theorem `Polynomial.coeff_sub` states that for any ring `R`, polynomials `p` and `q` in `R`, and a natural number `n`, the coefficient of `X^n` in the difference of `p` and `q` is equal to the difference of the coefficient of `X^n` in `p` and the coefficient of `X^n` in `q`. In mathematical terms, it means that if we subtract polynomial `q` from `p`, the `n`-th coefficient of the resultant polynomial is the difference between the `n`-th coefficients of `p` and `q`.
More concisely: For any ring R and polynomials p and q in R, the coefficient of X^n in p - q is equal to the coefficient of X^n in p - the coefficient of X^n in q.
|