monic_X_pow_add — Mathlib

English

If deg p ≤ n and coeff p n = 1, then p is monic.

Русский

Если deg p ≤ n и coeff p n = 1, то p моничен.

LaTeX

$$$\deg(p) \le n \land p.natCoeff(n) = 1 \Rightarrow p \text{ is monic}.$$$

Lean4

theorem monic_X_pow_add {n : ℕ} (H : degree p < n) : Monic (X ^ n + p) :=
  monic_of_degree_le n (le_trans (degree_add_le _ _) (max_le (degree_X_pow_le _) (le_of_lt H)))
    (by rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero])

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