monic_X_pow_sub_C

Mathlib.Algebra.Polynomial.Monic

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

← MathLib Explorer

English

For any a ∈ R and n ≠ 0, X^n − C a is monic.

Русский

Для любого a ∈ R и n ≠ 0 полином X^n − C a мононичен.

LaTeX

$$$\forall a : R, \forall n : \mathbb{N}, n \neq 0 \rightarrow Monic \left(X^n - C a\right)$$$

Lean4

/-- `X ^ n - a` is monic. -/
theorem monic_X_pow_sub_C {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) : (X ^ n - C a).Monic := by
  simpa only [map_neg, ← sub_eq_add_neg] using monic_X_pow_add_C (-a) h

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

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

Разделы

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

Аффилиация

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