degree_eq_zero_of_isUnit

Mathlib.Algebra.Polynomial.Degree.Units

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

← MathLib Explorer

English

If p is a unit in a semiring, then degree(p) = 0.

Русский

Если p является единицей в полупространстве, то degree(p) = 0.

LaTeX

$$$ IsUnit(p) \rightarrow degree(p) = 0 $$$

Lean4

theorem degree_eq_zero_of_isUnit [Nontrivial R] (h : IsUnit p) : degree p = 0 :=
  (natDegree_eq_zero_iff_degree_le_zero.mp <| natDegree_eq_zero_of_isUnit h).antisymm (zero_le_degree_iff.mpr h.ne_zero)

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

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

Разделы

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

Аффилиация

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