natDegree_pos_of_not_isUnit_of_dvd_monic

English

If p is monic, a is not a unit, and a divides p, then natDegree a > 0.

Русский

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

LaTeX

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

Lean4

theorem natDegree_pos_of_not_isUnit_of_dvd_monic (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < natDegree a :=
  natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_not_isUnit_of_dvd_monic hp ha hap

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