scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero

English

In a localization setting with a subring, if evaluating p at mk'(S,r,s) gives zero, then evaluating scaleRoots(p,s) at r also gives zero.

Русский

В локализационной обстановке: если вычисление p в mk'(S,r,s) равно нулю, то вычисление scaleRoots(p,s) в r равно нулю.

LaTeX

$$$\\aeval(\\mathrm{mk}' S\\, r\\, s)\\, p = 0 \\Rightarrow \\aeval(\\mathrm{algebraMap} A S\\, r)(\\mathrm{scaleRoots}(p,s)) = 0$$$

Lean4

theorem scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero {p : A[X]} {r : A} {s : M} (hr : aeval (mk' S r s) p = 0) :
    aeval (algebraMap A S r) (scaleRoots p s) = 0 :=
  by
  convert scaleRoots_eval₂_eq_zero (algebraMap A S) hr
  funext
  rw [aeval_def, mk'_spec' _ r s]

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