coeffs_ofSubring — Mathlib

English

All coefficients of the polynomial obtained by ofSubring lie inside the subring T.

Русский

Все коэффициенты полинома, полученного посредством ofSubring, лежат в подкольце T.

LaTeX

$$$(\\operatorname{coeffs}(\\mathrm{ofSubring}\\ T\\ p)).toSet \\subseteq T$$$

Lean4

@[simp]
theorem coeffs_ofSubring {p : T[X]} : (↑(p.ofSubring T).coeffs : Set R) ⊆ T := by
  classical
  intro i hi
  simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe, (Finset.coe_image)] at hi
  rcases hi with ⟨n, _, h'n⟩
  rw [← h'n, coeff_ofSubring]
  exact Subtype.mem (coeff p n : T)

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