monic_X_sub_C

Mathlib.Algebra.Polynomial.Monic

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

English

For every x in R, X − Cx is monic.

Русский

Для каждого x ∈ R полином X − Cx мононичен.

LaTeX

$$$\forall x : R, Monic \left(X - C x\right)$$$

Lean4

theorem monic_X_sub_C (x : R) : Monic (X - C x) := by simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)

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

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

Разделы

Аффилиация

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