scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero

English

A variant: if inj and hr, then aeval map equality for scaleRoots in divisor setting.

Русский

Вариант: при инъективности отображения и hr выполняется равенство aeval для scaleRoots в условиях делимости.

LaTeX

$$$\text{scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero}$$$

Lean4

theorem scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero [Algebra R K] (inj : Function.Injective (algebraMap R K))
    {p : R[X]} {r s : R} (hr : aeval (algebraMap R K r / algebraMap R K s) p = 0) (hs : s ∈ nonZeroDivisors R) :
    aeval (algebraMap R K r) (scaleRoots p s) = 0 :=
  scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero inj hr hs

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