monic_descPochhammer — Mathlib

English

For every n, descPochhammer R n is monic (leading coefficient 1) provided R has no zero divisors and is nontrivial.

Русский

Для каждого n полином descPochhammer R n является моноичным, если R не имеет нулевых делителей и ненулевой.

LaTeX

$$(descPochhammer R n).Monic$$

Lean4

theorem monic_descPochhammer (n : ℕ) [Nontrivial R] [NoZeroDivisors R] : Monic <| descPochhammer R n := by
  induction n with
  | zero => simp
  | succ n hn =>
    have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
    have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
    rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X, one_mul, one_mul, h,
      one_pow]

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