integralNormalization_eval₂_eq_zero

English

For p, f, z with hz = eval₂ f z p = 0, and inj property, eval₂ f (f p.leadingCoeff · z) (integralNormalization p) = 0.

Русский

Для p, f, z при hz = eval₂ f z p = 0 и инъективности, eval₂ f (f p.leadingCoeff · z) (integralNormalization p) = 0.

LaTeX

$$$hz = 0 \Rightarrow \operatorname{eval}_2 f (f(p.leadingCoeff) \cdot z) (\operatorname{integralNormalization}(p)) = 0$$$

Lean4

theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S} (hz : eval₂ f z p = 0)
    (inj : ∀ x : R, f x = 0 → x = 0) : eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0 :=
  integralNormalization_eval₂_eq_zero_of_commute _ hz (.all _ _) (.all _ _) inj

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