Polynomial.coeff_contract
theorem Polynomial.coeff_contract :
∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
p ≠ 0 → ∀ (f : Polynomial R) (n : ℕ), (Polynomial.contract p f).coeff n = f.coeff (n * p)
This theorem, `Polynomial.coeff_contract`, states that for any commutative semiring `R`, positive integer `p`, polynomial `f` over `R`, and natural number `n`, the coefficient of the term `X^n` in the contracted polynomial of `f` by `p` is equal to the coefficient of the term `X^(np)` in `f`. Here, the contraction operation on a polynomial transforms each term's exponent by dividing it by `p`, effectively "compressing" the polynomial.
More concisely: For any commutative semiring R, positive integer p, polynomial f over R in one variable X, and natural number n, the coefficient of X^(np) in polynomial f is equal to the coefficient of X^n in the polynomial obtained by contracting f by p.
|
Polynomial.coeff_expand
theorem Polynomial.coeff_expand :
∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
0 < p →
∀ (f : Polynomial R) (n : ℕ), ((Polynomial.expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0
This theorem, `Polynomial.coeff_expand`, states that for any given Type `R` which is an instance of `CommSemiring`, for any positive integer `p`, and for any Polynomial `f` of the type `R`, the coefficient of the `n`-th term of the expanded polynomial (where the polynomial is expanded by a factor of `p`) can be found as follows: if `p` is a divisor of `n`, then the coefficient is equal to the coefficient of the `(n / p)`-th term of the original polynomial `f`, otherwise, the coefficient is zero.
More concisely: For any commutative semiring R, positive integer p, and polynomial f over R, the coefficient of the n-th term in the polynomial f expanded by a factor of p is equal to the coefficient of the (n/p)-th term of the original polynomial f if p divides n, and is zero otherwise.
|
Polynomial.expand_C
theorem Polynomial.expand_C :
∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) (r : R), (Polynomial.expand R p) (Polynomial.C r) = Polynomial.C r
The theorem `Polynomial.expand_C` states that for any commutative semiring `R` and for any natural number `p` and element `r` of `R`, expanding the constant polynomial `r` by a factor of `p` is just the constant polynomial `r` itself. In mathematical terms, if `∑ aₙ xⁿ` is the general form of a polynomial, then expansion by a factor `p` turns it into `∑ aₙ xⁿᵖ`. Hence, if the polynomial is just a constant, `r`, then its expansion is also `r` since the expansion operation essentially does not affect constants.
More concisely: For any commutative semiring R and natural number p, expanding a constant polynomial r by a factor of p results in the constant polynomial r itself.
|
Polynomial.Monic.expand
theorem Polynomial.Monic.expand :
∀ {R : Type u} [inst : CommSemiring R] {p : ℕ} {f : Polynomial R},
0 < p → f.Monic → ((Polynomial.expand R p) f).Monic
This theorem states that for any commutative semiring `R`, any natural number `p` greater than zero, and any monic polynomial `f` over `R`, when the polynomial `f` is expanded by a factor of `p` using the `Polynomial.expand` function, the resulting polynomial is also monic. Here, a polynomial is considered monic if its leading coefficient is one. In mathematical notation, if we have a monic polynomial `f` such that `f = ∑ aₙ xⁿ`, expanding `f` by a factor of `p` means creating a new polynomial where each power `n` in `f` is replaced by `np`, i.e., `∑ aₙ xⁿᵖ`. The theorem asserts that the leading coefficient of this expanded polynomial is also one, hence it is also monic.
More concisely: For any commutative semiring `R`, if `p` is a positive natural number and `f` is a monic polynomial over `R`, then the polynomial obtained by expanding `f` by a factor of `p` using `Polynomial.expand` is also monic.
|
Polynomial.expand_X
theorem Polynomial.expand_X :
∀ {R : Type u} [inst : CommSemiring R] (p : ℕ), (Polynomial.expand R p) Polynomial.X = Polynomial.X ^ p
This theorem, `Polynomial.expand_X`, states that for any type `R` with an instance of `CommSemiring R` (i.e., `R` is a commutative semiring), and any natural number `p`, the operation of expanding the polynomial `Polynomial.X` (which is the polynomial variable or indeterminate) by a factor of `p` equals to the `p`-th power of `Polynomial.X`. In other words, if you take the polynomial `X` and apply the expansion operation with parameter `p`, the result will be `X` raised to the power of `p`. This operation is defined in the context of polynomial algebra.
More concisely: For any commutative semiring `R` and natural number `p`, expanding the polynomial variable `X` in `R` by a factor of `p` is equivalent to raising `X` to the power of `p`.
|
Polynomial.map_expand
theorem Polynomial.map_expand :
∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] {p : ℕ} {f : R →+* S}
{q : Polynomial R}, Polynomial.map f ((Polynomial.expand R p) q) = (Polynomial.expand S p) (Polynomial.map f q)
The theorem `Polynomial.map_expand` states that for any commutative semirings `R` and `S`, any natural number `p`, any ring homomorphism `f` from `R` to `S`, and any polynomial `q` over `R`, mapping the polynomial `q` expanded by a factor of `p` across the ring hom `f` is the same as expanding the polynomial obtained by mapping `q` across `f` by a factor of `p`. In other words, the operations of `Polynomial.map f` and `Polynomial.expand p` commute.
More concisely: For any commutative semirings R and S, natural number p, ring homomorphism f from R to S, and polynomial q over R, the expanded polynomial q with respect to p, mapped over f, is equal to the mapped polynomial obtained by expanding f(q) by p.
|
Polynomial.coeff_expand_mul
theorem Polynomial.coeff_expand_mul :
∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
0 < p → ∀ (f : Polynomial R) (n : ℕ), ((Polynomial.expand R p) f).coeff (n * p) = f.coeff n
This theorem states that for any commutative semiring `R`, any non-zero natural number `p`, any polynomial `f` over `R`, and any natural number `n`, if we expand the polynomial `f` by a factor of `p` to create a new polynomial, then the coefficient of `X^(n*p)` in the new expanded polynomial is the same as the coefficient of `X^n` in the original polynomial `f`. Essentially, the `Polynomial.coeff_expand_mul` theorem describes a property of polynomial expansion in the context of commutative semirings.
More concisely: For any commutative semiring `R`, polynomial `f` over `R`, natural number `p`, and `n`, the coefficient of `X^(n*p)` in the expanded polynomial `p*f` is equal to the coefficient of `X^n` in `f`.
|
Polynomial.expand_one
theorem Polynomial.expand_one :
∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R), (Polynomial.expand R 1) f = f
The theorem `Polynomial.expand_one` states that for any commutative semiring `R` and any polynomial `f` with coefficients in `R`, expanding the polynomial `f` by a factor of 1 results in the same polynomial `f`. In other words, if you take each term of the polynomial `f` and raise its variable part to the power of 1 (which is the operation of the `Polynomial.expand` function when the first argument is 1), the polynomial remains unchanged. This is consistent with the mathematical property that any number (or variable) raised to the power of 1 is the number (or variable) itself.
More concisely: For any commutative semiring R and polynomial f over R, expanding each term of f by 1 does not change the polynomial f.
|
Polynomial.expand_injective
theorem Polynomial.expand_injective :
∀ {R : Type u} [inst : CommSemiring R] {n : ℕ}, 0 < n → Function.Injective ⇑(Polynomial.expand R n)
This theorem states that the polynomial expansion operation is injective for any positive integer `n`. Specifically, if `R` is a type with an associated commutative semiring structure, and `n` is a positive natural number, then the function that expands a polynomial by a factor of `n` (i.e., transforms each term `aₙ xⁿ` into `aₙ xⁿᵖ`) is injective. That means, if two polynomials are expanded with the same factor `n` and the results are equal, then the original polynomials were also equal.
More concisely: For any commutative semiring `R` and positive integer `n`, the polynomial expansion by `n` is an injective function.
|