English
If 1 ≤ natDegree(p), then eval₂ f (f p.leadingCoeff · x) (integralNormalization p) equals f p.leadingCoeff^{natDegree(p) - 1} times p.eval₂ f x.
Русский
Если natDegree(p) ≥ 1, тогда eval₂ f (f(p.leadingCoeff)·x) от integralNormalization(p) равно f(p.leadingCoeff)^{natDegree(p) - 1} умножить на p.eval₂ f x.
LaTeX
$$$\operatorname{eval}_2^f( \operatorname{integralNormalization}(p), f(p.leadingCoeff) \cdot x) = f(p.leadingCoeff)^{(p.natDegree - 1)} \cdot p.\operatorname{eval}_2^f x$$$
Lean4
theorem integralNormalization_eval₂_leadingCoeff_mul_of_commute (h : 1 ≤ p.natDegree) (f : R →+* A) (x : A)
(h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r'}, Commute (f r) (f r')) :
(integralNormalization p).eval₂ f (f p.leadingCoeff * x) = f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x :=
by
rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]
apply Finset.sum_congr
· rw [natDegree_eq_of_degree_eq p.integralNormalization_degree]
intro n _hn
rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul, integralNormalization_coeff_mul_leadingCoeff_pow _ h,
f.map_mul, h₂.eq, f.map_pow, mul_assoc]
