not_isUnit_of_degree_pos — Mathlib

English

If a polynomial p ∈ R[X] has positive degree, then p is not a unit in R[X].

Русский

Если полином p ∈ R[X] имеет положительную степень, то он не является единицей в R[X].

LaTeX

$$$0 < \deg(p) \Rightarrow \lnot \IsUnit(p)$$$

Lean4

theorem not_isUnit_of_degree_pos (p : R[X]) (hpl : 0 < p.degree) : ¬IsUnit p :=
  by
  cases subsingleton_or_nontrivial R
  · simp [Subsingleton.elim p 0] at hpl
  intro h
  simp [degree_eq_zero_of_isUnit h] at hpl

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