coeff_multiset_prod_of_natDegree_le

English

For a multiset t of polynomials and a natural n, if natDegree(p) ≤ n for all p ∈ t, then coeff(t.prod, |t|·n) = ∏_{p∈t} coeff(p,n).

Русский

Для мультимножества t полиномов и натурального n, если для каждого p ∈ t выполнено natDegree(p) ≤ n, то коэффициент при степени |t|·n у произведения равен произведению коэффициентов p на степени n.

LaTeX

$$$$\left( \forall p \in t, \operatorname{natDegree}(p) \le n \right) \implies \operatorname{coeff}\left( t.prod, (|t|) \cdot n \right) = \prod_{p \in t} \operatorname{coeff}(p, n).$$$$

Lean4

theorem coeff_multiset_prod_of_natDegree_le (n : ℕ) (hl : ∀ p ∈ t, natDegree p ≤ n) :
    coeff t.prod ((Multiset.card t) * n) = (t.map fun p => coeff p n).prod :=
  by
  induction t using Quotient.inductionOn
  simpa using coeff_list_prod_of_natDegree_le _ _ hl

Похожие утверждения