English
The product of integralNormalization(p) with the polynomial C(leadingCoeff(p)) equals scaleRoots(p, leadingCoeff(p)).
Русский
Произведение integralNormalization(p) на C(leadingCoeff(p)) равно scaleRoots(p, leadingCoeff(p)).
LaTeX
$$$\operatorname{integralNormalization}(p) \cdot C(\operatorname{leadingCoeff}(p)) = \operatorname{scaleRoots}(p, \operatorname{leadingCoeff}(p))$$$
Lean4
theorem integralNormalization_mul_C_leadingCoeff (p : R[X]) :
integralNormalization p * C p.leadingCoeff = scaleRoots p p.leadingCoeff :=
by
ext i
rw [coeff_mul_C, integralNormalization_coeff]
split_ifs with h
· simp [natDegree_eq_of_degree_eq_some h, leadingCoeff]
· simp only [coeff_scaleRoots]
by_cases h' : i < p.degree
· rw [mul_assoc, ← pow_succ, tsub_right_comm, tsub_add_cancel_of_le]
rw [le_tsub_iff_left (coe_lt_degree.mp h').le, Nat.succ_le_iff]
exact coe_lt_degree.mp h'
· simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]
