monic_C_mul_of_mul_leadingCoeff_eq_one

Mathlib.Algebra.Polynomial.Monic

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

← MathLib Explorer

English

If deg p < n, then X^n + p is monic.

Русский

Если deg p < n, то X^n + p моничен.

LaTeX

$$$\deg(p) < n \Rightarrow \operatorname{Monic}(X^{n} + p).$$$

Lean4

theorem monic_C_mul_of_mul_leadingCoeff_eq_one {b : R} (hp : b * p.leadingCoeff = 1) : Monic (C b * p) :=
  by
  unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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

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

Разделы

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

Аффилиация

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