coeff_mem_contentIdeal

Mathlib.RingTheory.Polynomial.ContentIdeal

URI: https://scilib.ai/kg/mathlib#Polynomial.coeff_mem_contentIdeal

← MathLib Explorer

English

For every natural number n, the nth coefficient of p lies in the content ideal of p.

Русский

Для каждого натурального числа n коэффициент p принадлежит contentIdeal(m).

LaTeX

$$$p^{\}.coeff(n) \in p.contentIdeal$$$

Lean4

theorem coeff_mem_contentIdeal (n : ℕ) : p.coeff n ∈ p.contentIdeal :=
  by
  by_cases h : p.coeff n = 0
  · simp [h]
  · apply subset_span
    simpa using coeff_mem_coeffs h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru