map_monic_ne_zero

Mathlib.Algebra.Polynomial.Eval.Degree

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

English

If p is monic and S is nontrivial, then p.map f ≠ 0 for any ring hom f.

Русский

Если p монічен и S не тривиально, то p.map f ≠ 0 для любого кольцевого гомоморфизма f.

LaTeX

$$p.Monic → [Nontrivial S] → p.map f ≠ 0$$

Lean4

theorem map_monic_ne_zero (hp : p.Monic) [Nontrivial S] : p.map f ≠ 0 := fun h =>
  f.map_one_ne_zero ((map_monic_eq_zero_iff hp).mp h _)

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

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

Разделы

Аффилиация

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