scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero

English

If aeval (algebraMap r) p = 0 for some r, then aeval (algebraMap r) (scaleRoots p r) = 0.

Русский

Если aeval (algebraMap) p = 0, то aeval (algebraMap) (scaleRoots p r) = 0.

LaTeX

$$$\text{aeval}_{A}( \mathrm{algebraMap}(R, A)(r) ) (\operatorname{scaleRoots}(p, r)) = 0$ given the hypothesis.$$

Lean4

theorem scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero {p : S[X]} {f : S →+* K} (hf : Function.Injective f) {r s : S}
    (hr : eval₂ f (f r / f s) p = 0) (hs : s ∈ nonZeroDivisors S) : eval₂ f (f r) (scaleRoots p s) = 0 := by
  -- if we don't specify the type with `(_ : S)`, the proof is much slower

  nontriviality S using Subsingleton.eq_zero (_ : S)
  convert @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr
  rw [← mul_div_assoc, mul_comm, mul_div_cancel_right₀]
  exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs

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