coeff_minpolyDiv — Mathlib

English

The i-th coefficient of minpolyDiv satisfies a relation with the i+1 coefficient of minpoly via the base change X → x.

Русский

Для i-го коэффициента minpolyDiv существует зависимость через коэффициент minpoly на i+1 по замене X на x.

LaTeX

$$coeff (minpolyDiv R x) i = algebraMap R S (coeff (minpoly R x) (i+1)) + coeff (minpolyDiv R x) (i+1) * x$$

Lean4

theorem coeff_minpolyDiv (i) :
    coeff (minpolyDiv R x) i = algebraMap R S (coeff (minpoly R x) (i + 1)) + coeff (minpolyDiv R x) (i + 1) * x := by
  rw [← coeff_map, ← minpolyDiv_spec R x]; simp [mul_sub]

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