isMonicOfDegree_monomial_one — Mathlib

English

For any nontrivial R, the polynomial monomial n with coefficient 1 is monic of degree n.

Русский

Для не тривиального R многочлен монономом с коэффициентом 1 имеет степень n и мономичность.

LaTeX

$$IsMonicOfDegree_(monomial n 1) n$$

Lean4

theorem isMonicOfDegree_monomial_one (n : ℕ) : IsMonicOfDegree (monomial n (1 : R)) n := by
  simpa only [monomial_one_right_eq_X_pow] using isMonicOfDegree_X_pow R n

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