eval₂_minpolyDiv_of_eval₂_eq_zero

English

The natDegree of minpolyDiv plus 1 equals the natDegree of minpoly.

Русский

Порядковая степень natDegree(minpolyDiv x) + 1 равна natDegree(minpoly x).

LaTeX

$$natDegree (minpolyDiv R x) + 1 = natDegree (minpoly R x)$$

Lean4

theorem eval₂_minpolyDiv_of_eval₂_eq_zero {T} [CommRing T] [IsDomain T] [DecidableEq T] {x y} (σ : S →+* T)
    (hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0) :
    eval₂ σ y (minpolyDiv R x) = if σ x = y then σ (aeval x (derivative <| minpoly R x)) else 0 :=
  by
  split_ifs with h
  · rw [← h, eval₂_hom, eval_minpolyDiv_self]
  · rw [← eval₂_map, ← minpolyDiv_spec] at hy
    simpa [sub_eq_zero, Ne.symm h] using hy

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