eq_C_content_mul_primPart

Mathlib.RingTheory.Polynomial.Content

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

← MathLib Explorer

English

Every polynomial p can be written as p = C(content(p)) · p.primPart.

Русский

Каждый многочлен p можно представить как p = C(content(p)) · p.primPart.

LaTeX

$$$p = C\bigl(p.content\bigr) \cdot p.primPart$$$

Lean4

theorem eq_C_content_mul_primPart (p : R[X]) : p = C p.content * p.primPart :=
  by
  by_cases h : p = 0; · simp [h]
  rw [primPart, if_neg h, ← Classical.choose_spec (C_content_dvd p)]

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

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

Разделы

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

Аффилиация

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