eq_X_pow_iff_natTrailingDegree_eq_natDegree

English

For a monic p, p = X^{p.natDegree} iff p.natTrailingDegree = p.natDegree.

Русский

Для моноичного p выполняется: p = X^{p.natDegree} тогда p.natTrailingDegree = p.natDegree.

LaTeX

$$$ p.Monic \rightarrow (p = X^{p.natDegree} \iff p.natTrailingDegree = p.natDegree) $$$

Lean4

theorem eq_X_pow_iff_natTrailingDegree_eq_natDegree (h₁ : p.Monic) :
    p = X ^ p.natDegree ↔ p.natTrailingDegree = p.natDegree :=
  h₁.eq_X_pow_iff_natDegree_le_natTrailingDegree.trans (natTrailingDegree_le_natDegree p).ge_iff_eq

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