coeff_restriction — Mathlib

English

The coefficient of the restricted polynomial at n, when viewed as an element of R, equals the original coefficient of p at n.

Русский

Коэффициент ограниченного полинома при степени n совпадает с исходным коэффициентом p при степени n после естественного отображения.

LaTeX

$$$\uparrow(\operatorname{coeff}(\operatorname{restriction} p)\; n) = \operatorname{coeff} p\; n$$$

Lean4

@[simp]
theorem coeff_restriction {p : R[X]} {n : ℕ} : ↑(coeff (restriction p) n) = coeff p n := by
  classical
  simp only [restriction, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq', Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

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