scaleRoots_eval₂_eq_zero — Mathlib

English

If aeval a p = 0 in A, then aeval(algebraMap_R_A(r) * a) (scaleRoots p r) = 0 in A.

Русский

Если aeval a p = 0 в A, то aeval( algebraMap_R_A r · a ) (scaleRoots p r) = 0.

LaTeX

$$$\text{aeval}(a)\,p = 0 \;\Rightarrow\; \text{aeval}(\operatorname{algebraMap}(R, A)(r) \cdot a) (\operatorname{scaleRoots}(p, r)) = 0$$$

Lean4

theorem scaleRoots_eval₂_eq_zero {p : S[X]} (f : S →+* R) {r : R} {s : S} (hr : eval₂ f r p = 0) :
    eval₂ f (f s * r) (scaleRoots p s) = 0 := by rw [scaleRoots_eval₂_mul, hr, mul_zero]

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