comp_X_sub_C

Mathlib.Algebra.Polynomial.Monic

URI: https://scilib.ai/kg/mathlib#Polynomial.Monic.comp_X_sub_C

← MathLib Explorer

English

If f is injective and (p.map f) is monic, then p is monic.

Русский

Если f инъективен и (p.map f) мононичен, то p мононичен.

LaTeX

$$$\forall {R} {S} [\text{Semiring } R] [\text{Semiring } S] {f : R \rightarrow+* S} (hf : Injective f) {p : R[X]}, (p.map f).Monic \rightarrow p.Monic$$$

Lean4

theorem comp_X_sub_C {p : R[X]} (hp : p.Monic) (r : R) : (p.comp (X - C r)).Monic := by simpa using hp.comp_X_add_C (-r)

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

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

Разделы

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

Аффилиация

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