eval_minpolyDiv_self — Mathlib

English

For a RingHom σ₁ : S → T and σ₂ : S → T, the evaluation of minpolyDiv at σ₂ x with σ₁ is given by the if-then-else that distinguishes whether σ₁ x equals σ₂ x.

Русский

Для гомоморфизмов σ₁, σ₂ оценка minpolyDiv по σ₂ x с σ₁ равна условному выражению: если σ₁ x = σ₂ x, то особый образ; иначе 0.

LaTeX

$$eval₂ σ₁ (σ₂ x) (minpolyDiv R x) = iff(σ₁ x = σ₂ x) then σ₁ (aeval x (derivative (minpoly R x))) else 0$$

Lean4

theorem eval_minpolyDiv_self : (minpolyDiv R x).eval x = aeval x (derivative <| minpoly R x) := by
  rw [aeval_def, ← eval_map, ← derivative_map, ← minpolyDiv_spec R x]; simp

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