eq_X_pow_iff_natDegree_le_natTrailingDegree

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_natDegree_le_natTrailingDegree (h₁ : p.Monic) :
    p = X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · nontriviality R
    rw [h, natTrailingDegree_X_pow, ← h]
  · ext n
    rw [coeff_X_pow]
    obtain hn | rfl | hn := lt_trichotomy n p.natDegree
    · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)]
    · simpa only [if_pos rfl] using h₁.leadingCoeff
    · rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]

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