English
If evaluating p at z via f yields 0, and p.leadingCoeff commutes with z, and all f-r commute, then evaluating integralNormalization at f p.leadingCoeff times z yields 0.
Русский
Если eval₂ f z p = 0, и p.leadingCoeff commute с z, и все элементы полинома commute, то eval₂ f (f p.leadingCoeff · z) (integralNormalization p) = 0.
LaTeX
$$$\text{hz}:\; \operatorname{eval}_2 f z p = 0 \Rightarrow \operatorname{eval}_2 f (f(p.leadingCoeff) \cdot z) (\operatorname{integralNormalization}(p)) = 0$$$
Lean4
theorem integralNormalization_eval₂_eq_zero_of_commute {p : R[X]} (f : R →+* A) {z : A} (hz : eval₂ f z p = 0)
(h₁ : Commute (f p.leadingCoeff) z) (h₂ : ∀ {r r'}, Commute (f r) (f r')) (inj : ∀ x : R, f x = 0 → x = 0) :
eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0 :=
by
obtain (h | h) := p.natDegree.eq_zero_or_pos
· by_cases h0 : coeff p 0 = 0
· rw [eq_C_of_natDegree_eq_zero h]
simp [h0]
· rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz
exact absurd (inj _ hz) h0
· rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]
