sum_modByMonic_coeff — Mathlib

English

If q is monic and deg q ≤ n, then the sum of monomials with coefficients of p %ₘ q up to n equals p %ₘ q.

Русский

Если q мономический и deg q ≤ n, то сумма степенных мономов с коэффициентами p %ₘ q до n равна p %ₘ q.

LaTeX

$$$$ (\\sum_{i < n} i \\text{ such that } i \\in F_n) \\; \\text{monomial } i \\; ((p %ₘ q).coeff i) = p %ₘ q. $$$$

Lean4

theorem sum_modByMonic_coeff (hq : q.Monic) {n : ℕ} (hn : q.degree ≤ n) :
    (∑ i : Fin n, monomial i ((p %ₘ q).coeff i)) = p %ₘ q :=
  by
  nontriviality R
  exact
    (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans (sum_monomial_eq _)

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