coeff_prod_of_natDegree_le — Mathlib

English

For a finite set s and polynomials f_i with natDegree(f_i) ≤ n for all i ∈ s, we have coeff(∏_{i∈s} f_i, |s|·n) = ∏_{i∈s} coeff(f_i,n).

Русский

Для конечного множества s и полиномов f_i с natDegree(f_i) ≤ n для всех i ∈ s, коэффициент произведения при степени |s|·n равен произведению коэффициентов coeff(f_i,n).

LaTeX

$$$$\left( \forall i \in s, \operatorname{natDegree}(f(i)) \le n \right) \implies \operatorname{coeff}\left( \prod_{i\in s} f(i), |s|\cdot n \right) = \prod_{i\in s} \operatorname{coeff}(f(i), n).$$$$

Lean4

theorem coeff_prod_of_natDegree_le (f : ι → R[X]) (n : ℕ) (h : ∀ p ∈ s, natDegree (f p) ≤ n) :
    coeff (∏ i ∈ s, f i) (#s * n) = ∏ i ∈ s, coeff (f i) n :=
  by
  obtain ⟨l, hl⟩ := s
  convert coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
  · simp
  · simp
  · simpa using h

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