content_monomial

Mathlib.RingTheory.Polynomial.Content

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

← MathLib Explorer

English

The content of a monomial monomial k r equals normalize r.

Русский

Содержимое монома k r равно нормализованному r.

LaTeX

$$$$ content\\big(\\text{monomial } k \\; r\\big) = \\operatorname{normalize}(r) $$$$

Lean4

@[simp]
theorem content_monomial {r : R} {k : ℕ} : content (monomial k r) = normalize r := by
  rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_one]

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

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

Разделы

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

Аффилиация

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