English
The evaluation of minpolyDiv at x with σ₁, σ₂ reduces to a conditional formula depending on whether σ₁ x equals σ₂ x, identical to the previous lemma specialized to AlgHoms.
Русский
Значение minpolyDiv в x для алгебраических гомоморфизмов сводится к условному выражению в зависимости от равенства σ₁ x и σ₂ x.
LaTeX
$$eval₂_minpolyDiv_self$$
Lean4
theorem eval₂_minpolyDiv_self {T} [CommRing T] [Algebra R T] [IsDomain T] [DecidableEq T] (x : S) (σ₁ σ₂ : S →ₐ[R] T) :
eval₂ σ₁ (σ₂ x) (minpolyDiv R x) = if σ₁ x = σ₂ x then σ₁ (aeval x (derivative <| minpoly R x)) else 0 :=
by
apply eval₂_minpolyDiv_of_eval₂_eq_zero
rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom, eval_map, ← aeval_def,
minpoly.aeval, map_zero]
