contentIdeal_le_contentIdeal_of_dvd

Mathlib.RingTheory.Polynomial.ContentIdeal

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

← MathLib Explorer

English

If p divides q, then q.contentIdeal ≤ p.contentIdeal.

Русский

Если p делит q, то contentIdeal(q) ≤ contentIdeal(p).

LaTeX

$$$p \mid q \Rightarrow q.contentIdeal \le p.contentIdeal$$$

Lean4

theorem contentIdeal_le_contentIdeal_of_dvd (hpq : p ∣ q) : q.contentIdeal ≤ p.contentIdeal :=
  by
  obtain ⟨p', rfl⟩ := hpq
  exact le_trans (p.contentIdeal_mul_le_mul_contentIdeal p') mul_le_right

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

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

Разделы

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

Аффилиация

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