coeff_contract — Mathlib

English

For hp ≠ 0, (contract p f).coeff n = f.coeff (n p).

Русский

Для hp ≠ 0, коэффициент (contract p f) при n равен коэффициентf при n p.

LaTeX

$$$\bigl(\operatorname{contract}(p,f)\bigr).\mathrm{coeff} n = f.\mathrm{coeff}(n \cdot p)$$$

Lean4

theorem coeff_contract {p : ℕ} (hp : p ≠ 0) (f : R[X]) (n : ℕ) : (contract p f).coeff n = f.coeff (n * p) :=
  by
  simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt, ite_eq_left_iff]
  intro hn
  apply (coeff_eq_zero_of_natDegree_lt _).symm
  calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n)

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