not_isUnit_of_degree_pos_of_isReduced

English

For P ∈ R[X] over a reduced ring R, if deg(P) > 0, then P is not a unit.

Русский

Для полинома P ∈ R[X] над редуцированным кольцом R, если deg(P) > 0, то P не является единицей.

LaTeX

$$$ 0 < \operatorname{degree}(p) \Rightarrow \neg \operatorname{IsUnit}(p)$$$

Lean4

theorem not_isUnit_of_degree_pos_of_isReduced [IsReduced R] (p : R[X]) (hpl : 0 < p.degree) : ¬IsUnit p :=
  not_isUnit_of_natDegree_pos_of_isReduced _ (natDegree_pos_iff_degree_pos.mpr hpl)

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