Theorems · Theorem · field theory
Polynomial.coeff_mul
∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R) (n : ℕ),
(p * q).coeff n = ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, p.coeff x.1 * q.coeff x.2Decomposes the coefficient of the product p * q as a sum
over antidiagonal. A version which sums over range (n + 1) can be obtained
by using Finset.Nat.sum_antidiagonal_eq_sum_range_succ.
- Defined in
- Mathlib.Algebra.Polynomial.Coeff
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Polynomialstatement and proof · cited by 5,681
- Finset.sumstatement and proof · cited by 5,195
- Polynomial.coeffstatement and proof · cited by 1,045
- AddMonoidAlgebraproof · cited by 649
- Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
- Finset.HasAntidiagonal.mem_antidiagonalproof · cited by 51
- Polynomial.casesOnproof · cited by 15
- AddMonoidAlgebra.coeff_mul_antidiagproof · cited by 3
Cited by29
Results whose statement or proof uses this declaration.
- Polynomial.mul_coeff_zeroproof · cited by 37
- Polynomial.coeff_mul_X_powproof · cited by 9
- Ideal.mem_map_C_iffproof · cited by 6
- Polynomial.coeff_mul_X_pow'proof · cited by 5
- Polynomial.coeff_mul_degree_add_degreeproof · cited by 5
- Polynomial.coe_mulproof · cited by 3
- Polynomial.le_trailingDegree_mulproof · cited by 2
- Polynomial.mul_scaleRootsproof · cited by 2
- Polynomial.contentIdeal_mul_le_mul_contentIdealproof · cited by 2
- Polynomial.coeff_mul_add_eq_of_natDegree_leproof · cited by 2
- Nat.add_choose_eqproof · cited by 2
- MvPolynomial.pderiv_inl_universalFactorizationMap_Xproof · cited by 1