English
For i, if 1 ≤ natDegree(p), then coeff(integralNormalization(p), i) · leadingCoeff(p)^i = coeff(p,i) · leadingCoeff(p)^{natDegree(p) - 1}.
Русский
Пусть 1 ≤ natDegree(p). Тогда coeff(integralNormalization(p), i) · leadCoeff(p)^i = coeff(p,i) · leadCoeff(p)^{natDegree(p) - 1}.
LaTeX
$$$i \in \mathbb{N}, \ 1 \le \operatorname{natDegree}(p) \Rightarrow \operatorname{coeff}(\operatorname{integralNormalization}(p), i) \cdot (\operatorname{leadingCoeff}(p))^{i} = \operatorname{coeff}(p,i) \cdot (\operatorname{leadingCoeff}(p))^{(\operatorname{natDegree}(p) - 1)}$$$
Lean4
theorem integralNormalization_coeff_mul_leadingCoeff_pow (i : ℕ) (hp : 1 ≤ natDegree p) :
(integralNormalization p).coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1) :=
by
rw [integralNormalization_coeff]
split_ifs with h
·
simp [natDegree_eq_of_degree_eq_some h, leadingCoeff, ← pow_succ',
tsub_add_cancel_of_le (natDegree_eq_of_degree_eq_some h ▸ hp)]
· simp only [mul_assoc, ← pow_add]
by_cases h' : i < p.degree
· rw [tsub_add_cancel_of_le]
rw [le_tsub_iff_right hp, 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)]
