monic_of_natDegree_le_of_coeff_eq_one

English

If p is a polynomial with natDegree(p) ≤ n and p.coeff n = 1, then p is monic.

Русский

Если natDegree(p) ≤ n и коэффициент при x^n равен 1, тогда p монична.

LaTeX

$$$natDegree\le n \rightarrow (p.natDegree \le n) \, \wedge \, p.coeff(n) = 1 \Rightarrow p \text{ is Monic}$$$

Lean4

theorem monic_of_natDegree_le_of_coeff_eq_one (n : ℕ) (pn : p.natDegree ≤ n) (p1 : p.coeff n = 1) : Monic p :=
  by
  unfold Monic
  nontriviality
  refine (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn ?_).trans p1
  exact ne_of_eq_of_ne p1 one_ne_zero

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