degree_le_zero_iff_eq_one — Mathlib

English

Let p be a monic polynomial over a semiring. Then deg p ≤ 0 if and only if p = 1.

Русский

Пусть p — моноичная полином над полугруппой. Тогда deg p ≤ 0 тогда и только тогда p = 1.

LaTeX

$$$\text{Monic}(p) \Rightarrow (\deg p \le 0 \iff p = 1)$$$

Lean4

@[simp]
theorem degree_le_zero_iff_eq_one (hp : p.Monic) : p.degree ≤ 0 ↔ p = 1 := by
  rw [← hp.natDegree_eq_zero_iff_eq_one, natDegree_eq_zero_iff_degree_le_zero]

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