monic_X_pow_add_C

Mathlib.Algebra.Polynomial.Monic

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

← MathLib Explorer

English

If deg p < n, then X^n + p is monic (same as above).

Русский

Если deg p < n, то X^n + p моничен (аналогично выше).

LaTeX

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

Lean4

theorem monic_X_pow_add_C {n : ℕ} (h : n ≠ 0) : (X ^ n + C a).Monic :=
  monic_X_pow_add <|
    (lt_of_le_of_lt degree_C_le (by simp only [Nat.cast_pos, Nat.pos_iff_ne_zero, ne_eq, h, not_false_eq_true]))

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

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

Разделы

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

Аффилиация

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