coeff_ofSubring — Mathlib

English

For a polynomial p over a subring T, the coefficient of its image under the ofSubring construction at index n equals the coefficient of p at n, viewed in T.

Русский

Коэффициент полинома в подкольце T после применения ofSubring на позиции n равен коэффициенту p на позиции n, рассматриваемому в T.

LaTeX

$$$\\operatorname{coeff}(\\mathrm{ofSubring}\\ T\\ p)\\ n = \\operatorname{coeff}(p)\\ n$ в T$$

Lean4

theorem coeff_ofSubring (p : T[X]) (n : ℕ) : coeff (ofSubring T p) n = (coeff p n : T) :=
  by
  simp only [ofSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq', Ne, Classical.not_not,
    ite_eq_left_iff]
  intro h
  rw [h, ZeroMemClass.coe_zero]

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