Lemmas for the interaction between polynomials and ∑
and ∏
. #
Recall that ∑
and ∏
are notation for finset.sum
and finset.prod
respectively.
Main results #
polynomial.nat_degree_prod_of_monic
: the degree of a product of monic polynomials is the product of degrees. We prove this only for[comm_semiring R]
, but it ought to be true for[semiring R]
andlist.prod
.polynomial.nat_degree_prod
: for polynomials over an integral domain, the degree of the product is the sum of degrees.polynomial.leading_coeff_prod
: for polynomials over an integral domain, the leading coefficient is the product of leading coefficients.polynomial.prod_X_sub_C_coeff_card_pred
carries most of the content for computing the second coefficient of the characteristic polynomial.
The degree of a product of polynomials is at most the sum of the degrees, where the degree of the zero polynomial is ⊥.
The leading coefficient of a product of polynomials is equal to the product of the leading coefficients, provided that this product is nonzero.
See polynomial.leading_coeff_multiset_prod
(without the '
) for a version for integral domains,
where this condition is automatically satisfied.
The leading coefficient of a product of polynomials is equal to the product of the leading coefficients, provided that this product is nonzero.
See polynomial.leading_coeff_prod
(without the '
) for a version for integral domains,
where this condition is automatically satisfied.
The degree of a product of polynomials is equal to the sum of the degrees, provided that the product of leading coefficients is nonzero.
See polynomial.nat_degree_multiset_prod
(without the '
) for a version for integral domains,
where this condition is automatically satisfied.
The degree of a product of polynomials is equal to the sum of the degrees, provided that the product of leading coefficients is nonzero.
See polynomial.nat_degree_prod
(without the '
) for a version for integral domains,
where this condition is automatically satisfied.
The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
[nontrivial R]
is needed, otherwise for l = []
we have ⊥
in the LHS and 0
in the RHS.
The degree of a product of polynomials is equal to the sum of the degrees.
See polynomial.nat_degree_prod'
(with a '
) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
The degree of a product of polynomials is equal to the sum of the degrees, where the degree of the zero polynomial is ⊥.
The degree of a product of polynomials is equal to the sum of the degrees, where the degree of the zero polynomial is ⊥.
The leading coefficient of a product of polynomials is equal to the product of the leading coefficients.
See polynomial.leading_coeff_multiset_prod'
(with a '
) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
The leading coefficient of a product of polynomials is equal to the product of the leading coefficients.
See polynomial.leading_coeff_prod'
(with a '
) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.