minpolyDiv — Mathlib

English

The polynomial minpolyDiv R x is defined as the quotient of minpoly R x by the divisor X − C x after mapping coefficients into S.

Русский

Полином minpolyDiv R x определяется как частное полинома minpoly R x на делитель X − C x после отображения коэффициентов в S.

LaTeX

$$minpolyDiv R x := (minpoly R x).map (algebraMap R S) /ₘ (X - C x)$$

Lean4

/-- `minpolyDiv R x : S[X]` for `x : S` is the polynomial `minpoly R x / (X - C x)`. -/
noncomputable def minpolyDiv : S[X] :=
  (minpoly R x).map (algebraMap R S) /ₘ (X - C x)

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