Polynomial.Monic.degree_le_zero_iff_eq_one
theorem Polynomial.Monic.degree_le_zero_iff_eq_one :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → (p.degree ≤ 0 ↔ p = 1)
The theorem `Polynomial.Monic.degree_le_zero_iff_eq_one` states that for any polynomial `p` over a semiring `R`, if `p` is a monic polynomial (i.e., its leading coefficient is 1), then the degree of `p` is less than or equal to 0 if and only if `p` is equal to 1. In other words, for a monic polynomial, having a degree that is zero or negative is equivalent to it being the polynomial 1.
More concisely: A monic polynomial over a semiring has degree less than or equal to 0 if and only if it equals the constant polynomial 1.
|
Polynomial.monic_prod_of_monic
theorem Polynomial.monic_prod_of_monic :
∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (s : Finset ι) (f : ι → Polynomial R),
(∀ i ∈ s, (f i).Monic) → (s.prod fun i => f i).Monic
This theorem states that for any type `R` with a commutative semiring structure, and any finite set `s` of an arbitrary type `ι`, if you have a function `f` that assigns to each element of `s` a monic polynomial (i.e., a polynomial with leading coefficient 1), then the product of all these polynomials (where the product is taken over all elements of `s`) is also a monic polynomial. In other words, the product of monic polynomials, produced over a finite set, is always a monic polynomial.
More concisely: Given a commutative semiring `R` and a finite set `s` of any type, if for each element `x` in `s`, we have a monic polynomial `p_x` in `R[x]`, then the product of `p_x` over all `x` in `s` is a monic polynomial in `R[x_1, ..., x_n]`.
|
Polynomial.monic_multiset_prod_of_monic
theorem Polynomial.monic_multiset_prod_of_monic :
∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R),
(∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
The theorem `Polynomial.monic_multiset_prod_of_monic` states that for any type `R`, given a commutative semiring structure on `R`, and any other type `ι`, if we have a multiset `t` of type `ι` and a function `f` from `ι` to `Polynomial R`, then if every polynomial `f i` for `i` in `t` is monic (i.e., its leading coefficient is 1), then the polynomial obtained by taking the product of the multiset obtained by mapping `f` over `t` is also monic. In other words, the product of a collection of monic polynomials is itself a monic polynomial.
More concisely: Given a commutative semiring `R`, a multiset `t` of indices `ι`, and a function `f` mapping each index `i` in `t` to a monic polynomial `f i` in `Polynomial R`, the product of `f i` for all `i` in `t` is a monic polynomial in `Polynomial R`.
|
Polynomial.eq_of_monic_of_associated
theorem Polynomial.eq_of_monic_of_associated :
∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q.Monic → Associated p q → p = q
This theorem states that for any semiring `R`, if `p` and `q` are polynomials over `R`, and both `p` and `q` are monic (i.e., their leading coefficients are 1), then if `p` and `q` are associated (meaning that one can be obtained from the other by multiplication with a unit), it must be the case that `p` is equal to `q`. This establishes a limiting condition on the "associated" relationship for monic polynomials, implying that if two monic polynomials are associated, they must actually be the same polynomial.
More concisely: For any semiring `R`, if `p` and `q` are monic polynomials over `R`, then `p = q` whenever `p` and `q` are associates.
|
Polynomial.monic_X_sub_C
theorem Polynomial.monic_X_sub_C : ∀ {R : Type u} [inst : Ring R] (x : R), (Polynomial.X - Polynomial.C x).Monic := by
sorry
The theorem `Polynomial.monic_X_sub_C` states that for any type `R` equipped with a ring structure (denoted by `inst : Ring R`) and for any element `x` in `R`, the polynomial `X - Cx` (representing the polynomial with variable `X` minus the constant polynomial of `x`) is monic. In mathematical terms, the leading coefficient of the polynomial `X - Cx` is always 1, irrespective of the ring `R` and the element `x` in `R`.
More concisely: For any ring `R` and element `x` in `R`, the polynomial `X - Cx` is monic (has a leading coefficient of 1).
|
Polynomial.Monic.natDegree_mul'
theorem Polynomial.Monic.natDegree_mul' :
∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
p.Monic → q ≠ 0 → (p * q).natDegree = p.natDegree + q.natDegree
The theorem `Polynomial.Monic.natDegree_mul'` states that for any type `R` that is a semiring, and for any two polynomials `p` and `q` over that semiring, if the polynomial `p` is monic (i.e., its leading coefficient is 1) and the polynomial `q` is not zero, then the natural degree (the degree forced to ℕ with the degree of 0 defined as 0) of the product of `p` and `q` is equal to the sum of the natural degrees of `p` and `q`. In mathematical terms, for monic `p` and non-zero `q`, we have $\deg(p*q) = \deg(p) + \deg(q)$.
More concisely: For any monic polynomial `p` and non-zero polynomial `q` over a semiring, the natural degree of their product is equal to the sum of their natural degrees.
|
Polynomial.Monic.map
theorem Polynomial.Monic.map :
∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
p.Monic → (Polynomial.map f p).Monic
This theorem states that for any types `R` and `S` equipped with semiring structures, any polynomials `p` over `R`, and any ring homomorphism `f` from `R` to `S`, if the polynomial `p` is `Monic` (that is, its leading coefficient is 1), then the polynomial obtained by mapping `p` across the ring homomorphism `f` (denoted as `Polynomial.map f p`) is also `Monic`. In other words, the property of being `Monic` is preserved under the operation of mapping polynomials via a ring homomorphism.
More concisely: If `f` is a ring homomorphism from semiring `R` to semiring `S`, `p` is a monic polynomial over `R`, then `Polynomial.map f p` is a monic polynomial over `S`.
|
Polynomial.natDegree_map_eq_of_injective
theorem Polynomial.natDegree_map_eq_of_injective :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).natDegree = p.natDegree
This theorem states that for any types `R` and `S` that are both instances of a semiring, and for any injective ring homomorphism `f` from `R` to `S`, the natural degree of the polynomial obtained by mapping a polynomial `p` over `R` with `f` is equal to the natural degree of the original polynomial `p`. In mathematical terms, if `f : R → S` is an injective ring homomorphism and `p` is a polynomial over `R`, then the degree of the polynomial `f(p)` in `S` is the same as the degree of `p` in `R`.
More concisely: For any injective ring homomorphism between semirings `f : R → S` and polynomial `p` over `R`, the degree of `f(p)` over `S` equals the degree of `p` over `R`.
|
Polynomial.degree_map_eq_of_injective
theorem Polynomial.degree_map_eq_of_injective :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).degree = p.degree
This theorem states that for any semirings `R` and `S`, and for any injective ring homomorphism `f` from `R` to `S`, the degree of any polynomial `p` from `R` remains the same after mapping `p` across the homomorphism `f`. In other words, if you have a polynomial with coefficients in a semiring `R` and you map it to a polynomial with coefficients in a semiring `S` using an injective homomorphism, the degree of the polynomial does not change.
More concisely: For any injective ring homomorphism `f` from semiring `R` to semiring `S`, the degree of any polynomial `p` in `R` equals the degree of `f(p)` in `S`.
|
Polynomial.Monic.pow
theorem Polynomial.Monic.pow :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ (n : ℕ), (p ^ n).Monic
This theorem states that for any polynomial `p` in a semiring `R`, if `p` is monic (i.e., its leading coefficient is 1), then any natural number power of `p` is also monic. Essentially, it's saying that raising a monic polynomial to any power doesn't change the property of being monic.
More concisely: If `p` is a monic polynomial in a semiring `R`, then for all natural numbers `n`, `p^n` is also a monic polynomial in `R`.
|
Polynomial.monic_X_pow_sub_C
theorem Polynomial.monic_X_pow_sub_C :
∀ {R : Type u} [inst : Ring R] (a : R) {n : ℕ}, n ≠ 0 → (Polynomial.X ^ n - Polynomial.C a).Monic
The theorem `Polynomial.monic_X_pow_sub_C` states that for any ring `R`, any element `a` from `R`, and any natural number `n` different from zero, the polynomial `X^n - a` is monic, i.e., its leading coefficient is 1. Here, `X` represents the polynomial variable and `C a` denotes the constant polynomial `a`.
More concisely: For any ring `R`, `X^n - C a` is a monic polynomial in `R[X]` for any `a` in `R` and natural number `n` different from zero.
|
Polynomial.Monic.natDegree_map
theorem Polynomial.Monic.natDegree_map :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Nontrivial S] {P : Polynomial R},
P.Monic → ∀ (f : R →+* S), (Polynomial.map f P).natDegree = P.natDegree
The theorem `Polynomial.Monic.natDegree_map` states that for any semirings `R` and `S`, with `S` being nontrivial, and for any monic polynomial `P` over `R`, the degree of the polynomial obtained by mapping `P` across a ring homomorphism `f : R →+* S` is the same as the degree of `P`. In other words, the natural degree of a monic polynomial remains the same under ring homomorphism mapping.
More concisely: For any monic polynomial $P$ over a semiring $R$, and any nontrivial ring homomorphism $f : R \to S$, the degree of $P$ and the degree of $P$ mapped under $f$ are equal.
|
Polynomial.Monic.nextCoeff_multiset_prod
theorem Polynomial.Monic.nextCoeff_multiset_prod :
∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R),
(∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
The theorem `Polynomial.Monic.nextCoeff_multiset_prod` states that for any commutative semiring `R` and any type `ι`, given a multiset `t` of `ι` and a function `f` from `ι` to `Polynomial R` such that every polynomial `f i` for `i` in `t` is monic, the second highest coefficient (or 0 for constants) of the product of the multiset obtained by mapping `f` on `t` is equal to the sum of the multisets obtained by mapping the function that gets the second highest coefficient from `f i` for each `i` in `t`. In simpler terms, this means that if we have a multiset of monic polynomials, the next coefficient of the product of these polynomials is the sum of the next coefficients of each polynomial in the multiset.
More concisely: Given a commutative semiring R and a multiset t of indices, if f maps each i in t to a monic polynomial, then the second highest coefficient of the product of f(i) is the sum of the second highest coefficients of f(i) for all i in t.
|
Polynomial.Monic.mul_left_eq_zero_iff
theorem Polynomial.Monic.mul_left_eq_zero_iff :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ {q : Polynomial R}, q * p = 0 ↔ q = 0
This theorem states that for any semiring `R` and any polynomial `p` over `R` that is monic (i.e., its leading coefficient is 1), the product of `p` and any other polynomial `q` over `R` is zero if and only if `q` is zero. In other words, if `p` is a monic polynomial, then it has the property that multiplying it by another polynomial `q` results in a zero polynomial precisely when `q` is a zero polynomial.
More concisely: For any semiring `R` and monic polynomial `p` over `R`, `p * q = 0` if and only if `q = 0`.
|
Polynomial.Monic.natDegree_eq_zero_iff_eq_one
theorem Polynomial.Monic.natDegree_eq_zero_iff_eq_one :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → (p.natDegree = 0 ↔ p = 1)
The theorem `Polynomial.Monic.natDegree_eq_zero_iff_eq_one` states that for any type `R` that forms a semiring, and for any monic polynomial `p` of type `R`, the natural degree of `p` is zero if and only if `p` equals one. In other words, a monic polynomial in a semiring has a natural degree of zero precisely when the polynomial itself is equal to one.
More concisely: For any monic polynomial `p` in a semiring R, the natural degree of `p` is equal to zero if and only if `p` equals the constant polynomial 1.
|
Polynomial.monic_X_add_C
theorem Polynomial.monic_X_add_C : ∀ {R : Type u} [inst : Semiring R] (x : R), (Polynomial.X + Polynomial.C x).Monic
This theorem states that for any type `R` which is a semiring, and any value `x` of type `R`, the polynomial `X + Cx` is monic. In other words, if we add a polynomial variable `X` and a constant polynomial `Cx` in a semiring `R`, the leading coefficient of the resulting polynomial is 1, which is the definition of a monic polynomial.
More concisely: For any semiring `R` and `x` in `R`, the polynomial `X + Cx` is monic (has a leading coefficient of 1).
|
Polynomial.Monic.eq_one_of_isUnit
theorem Polynomial.Monic.eq_one_of_isUnit :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → IsUnit p → p = 1
The theorem `Polynomial.Monic.eq_one_of_isUnit` states that for all types `R` that have a semiring structure, for any polynomial `p` over `R`, if `p` is a monic polynomial and `p` is a unit (i.e., it has a two-sided inverse), then `p` is equal to the polynomial `1`. In mathematical terms, given a polynomial `p` in a semiring `R`, if the leading coefficient of `p` is `1` and there exists an element `q` in `R` such that `p*q = 1` and `q*p = 1`, then `p` is the polynomial `1`.
More concisely: If `p` is a monic polynomial over a semiring `R` with a two-sided inverse, then `p = 1`.
|