eq_one_of_monic_natDegree_zero

Mathlib.Algebra.Polynomial.Degree.Operations

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

← MathLib Explorer

English

If p is monic and natDegree p = 0, then p = 1.

Русский

Если p монический и natDegree p = 0, то p = 1.

LaTeX

$$$ p.Monic \rightarrow p.natDegree = 0 \rightarrow p = 1. $$$

Lean4

theorem eq_one_of_monic_natDegree_zero (hf : p.Monic) (hfd : p.natDegree = 0) : p = 1 :=
  by
  rw [Monic.def, leadingCoeff, hfd] at hf
  rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]

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

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

Разделы

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

Аффилиация

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