Polynomial.natDegree_prod'
theorem Polynomial.natDegree_prod' :
∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
(s.prod fun i => (f i).leadingCoeff) ≠ 0 → (s.prod fun i => f i).natDegree = s.sum fun i => (f i).natDegree
This theorem states that in a commutative semiring, for a finite set of polynomials, if the product of their leading coefficients is not zero, then the degree of the product of these polynomials is equal to the sum of their individual degrees. The theorem provides an alternative to `Polynomial.natDegree_prod`, which applies to integral domains, where the condition of non-zero product of leading coefficients is always met.
More concisely: In a commutative semiring, if the leading coefficients of a finite product of polynomials are non-zero, then the degree of their product is equal to the sum of their individual degrees.
|
Polynomial.leadingCoeff_multiset_prod
theorem Polynomial.leadingCoeff_multiset_prod :
∀ {R : Type u} [inst : CommSemiring R] [inst_1 : NoZeroDivisors R] (t : Multiset (Polynomial R)),
t.prod.leadingCoeff = (Multiset.map (fun f => f.leadingCoeff) t).prod
This theorem states that for any multiset `t` of polynomials over a commutative semiring `R` with no zero divisors, the leading coefficient of the product of the polynomials in `t` is equal to the product of the leading coefficients of the polynomials in `t`. In mathematical terms, if the leading coefficient of a polynomial `f` is denoted by `f.leadingCoeff`, then the leading coefficient of the product of a set of polynomials `f_1, f_2, ..., f_n` is the product of `f_1.leadingCoeff, f_2.leadingCoeff, ..., f_n.leadingCoeff`. There is a similar version of this theorem for commutative semirings where additionally, the product of the leading coefficients must be nonzero.
More concisely: For any multiset of polynomials over a commutative semiring with no zero divisors, the product of their leading coefficients is equal to the leading coefficient of their product.
|
Polynomial.leadingCoeff_prod'
theorem Polynomial.leadingCoeff_prod' :
∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
(s.prod fun i => (f i).leadingCoeff) ≠ 0 →
(s.prod fun i => f i).leadingCoeff = s.prod fun i => (f i).leadingCoeff
This theorem states that for any commutative semiring `R`, given a finite set `s` and a function `f` that outputs a polynomial in `R` for each element in `s`, if the product of the leading coefficients of the polynomials is nonzero, then the leading coefficient of the product of the polynomials is equal to the product of the leading coefficients of the polynomials. There is a version of this theorem for integral domains where the condition of the product of leading coefficients being nonzero is automatically satisfied.
More concisely: Given a commutative semiring `R`, a finite set `s`, and a function `f` mapping `s` to polynomials in `R` with nonzero leading coefficients, the leading coefficient of the product of `f(x)` for `x` in `s` is equal to the product of their leading coefficients.
|
Polynomial.natDegree_multiset_prod'
theorem Polynomial.natDegree_multiset_prod' :
∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
(Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 →
t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
This theorem states that given a commutative semiring `R` and a multiset of polynomials over `R`, if the product of the leading coefficients of the polynomials in the multiset is nonzero, then the degree of the product of all polynomials in the multiset equals the sum of the degrees of all individual polynomials in the multiset. This is the general case theorem, there's another version specifically for integral domains where the condition about leading coefficient product being nonzero is automatically fulfilled.
More concisely: Given a commutative semiring `R` and a multiset of polynomials over `R`, if the product of their leading coefficients is nonzero, then the degree of their product equals the sum of their individual degrees.
|
Polynomial.degree_prod
theorem Polynomial.degree_prod :
∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] [inst_1 : NoZeroDivisors R]
(f : ι → Polynomial R) [inst_2 : Nontrivial R], (s.prod fun i => f i).degree = s.sum fun i => (f i).degree
This theorem states that for any commutative semiring `R` with no zero divisors and a nontrivial element, given a finite set `s` and a function `f` mapping each element of `s` to a polynomial over `R`, the degree of the product of all polynomials (obtained by applying `f` to each element of `s` and then taking the product) is equal to the sum of the degrees of these individual polynomials. This holds true even when the polynomial is the zero polynomial, in which case its degree is defined to be ⊥ (bottom).
More concisely: For any commutative semiring without zero divisors and a finite set, the degree of the product of polynomials, each obtained by mapping an element to a polynomial over the semiring, equals the sum of the degrees of these individual polynomials. This holds for the zero polynomial with degree ⊥ (bottom).
|
Polynomial.natDegree_prod
theorem Polynomial.natDegree_prod :
∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] [inst_1 : NoZeroDivisors R]
(f : ι → Polynomial R), (∀ i ∈ s, f i ≠ 0) → (s.prod fun i => f i).natDegree = s.sum fun i => (f i).natDegree
The theorem `Polynomial.natDegree_prod` states that for any commutative semiring `R` with no zero divisors and any finset `s` of indices `ι`, if for every index `i` in `s`, the corresponding polynomial `f(i)` is non-zero, then the degree of the product of these polynomials is equal to the sum of their individual degrees. An alternative version of this theorem for commutative semirings where the product of the leading coefficients is non-zero is given by `Polynomial.natDegree_prod'`.
More concisely: For any commutative semiring with no zero divisors and a finset of non-zero polynomials, the degree of their product equals the sum of their individual degrees.
|
Polynomial.leadingCoeff_prod
theorem Polynomial.leadingCoeff_prod :
∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] [inst_1 : NoZeroDivisors R]
(f : ι → Polynomial R), (s.prod fun i => f i).leadingCoeff = s.prod fun i => (f i).leadingCoeff
The theorem `Polynomial.leadingCoeff_prod` states that for any finite set `s` and any function `f` mapping elements of `s` to polynomials over a commutative semiring `R` that has no zero divisors, the leading coefficient of the product of polynomials (obtained by applying `f` to each element of `s` and taking the product) is equal to the product of the leading coefficients of these polynomials. In other words, when we multiply polynomials together, the leading coefficient of the result is just the product of the leading coefficients of the individual polynomials.
There is an alternative version of this theorem (`Polynomial.leadingCoeff_prod'`) for commutative semirings where the product of the leading coefficients must additionally be nonzero.
More concisely: For any finite set and a function mapping elements to polynomials over a commutative semiring without zero divisors, the leading coefficients of the polynomials formed by applying the function to each element and taking the product equal the product of the leading coefficients of the individual polynomials. (Or, similarly, for commutative semirings where the product of the leading coefficients is nonzero: the leading coefficient of the product of polynomials is the product of their leading coefficients.)
|
Polynomial.degree_multiset_prod
theorem Polynomial.degree_multiset_prod :
∀ {R : Type u} [inst : CommSemiring R] [inst_1 : NoZeroDivisors R] (t : Multiset (Polynomial R))
[inst_2 : Nontrivial R], t.prod.degree = (Multiset.map (fun f => f.degree) t).sum
The theorem `Polynomial.degree_multiset_prod` states that the degree of a product of polynomials is equal to the sum of the degrees of the polynomials in the product. Here, the degree of the zero polynomial is considered as bottom (⊥). This theorem holds for any polynomial over a commutative semiring `R` with no zero divisors and nontrivial coefficients. In the context of the theorem, a `Multiset` of polynomials is used, where a `Multiset` is a type representing a finite set that allows duplicates. The `map` function on `Multiset` is used to create a new `Multiset` where each polynomial's degree is calculated. The `sum` operation then adds up all these degrees.
More concisely: The theorem asserts that the degree of a product of polynomials over a commutative semiring without zero divisors is equal to the sum of the degrees of the polynomials in the product. (Here, the degree of the zero polynomial is considered as bottom.)
|
Polynomial.leadingCoeff_multiset_prod'
theorem Polynomial.leadingCoeff_multiset_prod' :
∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
(Multiset.map Polynomial.leadingCoeff t).prod ≠ 0 →
t.prod.leadingCoeff = (Multiset.map Polynomial.leadingCoeff t).prod
The theorem `Polynomial.leadingCoeff_multiset_prod'` states that, for any commutative semiring `R` and a multiset `t` of polynomials over `R`, if the product of the leading coefficients of the polynomials in `t` is non-zero, then the leading coefficient of the product of the polynomials in `t` is equal to the product of the leading coefficients. This theorem also suggests referring to `Polynomial.leadingCoeff_multiset_prod` for a version for integral domains, where the condition of the product of the leading coefficients being non-zero is automatically satisfied.
More concisely: If `R` is a commutative semiring and `t` is a multiset of polynomials over `R` with non-zero product of leading coefficients, then the leading coefficient of the product of polynomials in `t` is equal to the product of their leading coefficients.
|
Polynomial.degree_multiset_prod_le
theorem Polynomial.degree_multiset_prod_le :
∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
t.prod.degree ≤ (Multiset.map Polynomial.degree t).sum
This theorem states that for any multiset `t` of polynomials over a commutative semiring `R`, the degree of the product of all polynomials in `t` is less than or equal to the sum of the degrees of all the polynomials in `t`. Here, the degree of a polynomial is the highest power of `X` that appears in it, and the degree of the zero polynomial is considered as `⊥` (bottom). The function `Multiset.map Polynomial.degree t` creates a new multiset by mapping each polynomial in `t` to its degree, and then the sum of all elements in this multiset is computed. The theorem is then saying that the degree of the product polynomial is always less than or equal to this sum.
More concisely: For any multiset of polynomials over a commutative semiring, the degree of their product is less than or equal to the sum of the degrees of the individual polynomials.
|
Polynomial.degree_list_prod
theorem Polynomial.degree_list_prod :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] [inst_2 : Nontrivial R] (l : List (Polynomial R)),
l.prod.degree = (List.map Polynomial.degree l).sum
The theorem `Polynomial.degree_list_prod` states that for any list of polynomials `l` over a ring `R` that has no zero divisors and is nontrivial, the degree of the product of the polynomials in `l` is equal to the sum of the degrees of the polynomials in `l`. Here, the degree of a polynomial is considered as the largest exponent of 'X' in the polynomial, with the degree of the zero polynomial defined as `⊥`. The condition of `R` being nontrivial is required to handle the edge case when `l` is an empty list, where the left-hand side of the equation would be `⊥` and the right-hand side would be `0`.
More concisely: For any list of polynomials over a nontrivial ring without zero divisors, the degree of their product equals the sum of their degrees.
|