degree_pos — Mathlib

English

For a monic polynomial p over a commutative semiring, degree p > 0 if and only if p ≠ 1.

Русский

Для монического многочлена p над коммутативной полусистемой, deg(p) > 0 тогда и только тогда, когда p ≠ 1.

LaTeX

$$$\deg(p) > 0 \iff p \neq 1 \quad\text{при } p\text{ монический}$$$

Lean4

theorem degree_pos : 0 < degree p ↔ p ≠ 1 :=
  natDegree_pos_iff_degree_pos.symm.trans hp.natDegree_pos

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