degree_pos_of_ne_zero_of_nonunit — Mathlib

English

If p ∈ DivisionRing R[X] is nonzero and not a unit, then deg p > 0.

Русский

Если p ≠ 0 и не является единицей, то deg p > 0.

LaTeX

$$$p \neq 0 \ \wedge\ \lnot \text{IsUnit}(p) \implies 0 < \deg(p).$$$

Lean4

theorem degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 < degree p :=
  lt_of_not_ge fun h => by
    rw [eq_C_of_degree_le_zero h] at hp0 hp
    exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))

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