degree_pos_of_not_isUnit_of_dvd_monic

English

If p is monic, a is not a unit, and a divides p, then deg(a) > 0.

Русский

Если p моничен, a не единица, и a делит p, то deg(a) > 0.

LaTeX

$$$p.Monic \rightarrow \lnot IsUnit(a) \rightarrow a \mid p \rightarrow 0 < degree(a)$$$

Lean4

theorem degree_pos_of_not_isUnit_of_dvd_monic (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < degree a :=
  by
  contrapose! ha with h
  rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢
  simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap

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