English
For a polynomial p over S, the function coeffIntegerNormalization picks the R-coefficient corresponding to i if i is in the support of p, and 0 otherwise.
Русский
Для полинома p над S функция coeffIntegerNormalization выбирает коэффициент в R при индексе i, если i принадлежит поддержке p, иначе 0.
LaTeX
$$$\text{coeffIntegerNormalization }(M,p,i) = \begin{cases} \text{chosen init}, & i \in \mathrm{supp}(p) \\ 0, & \text{otherwise} \end{cases}$$$
Lean4
/-- `coeffIntegerNormalization p` gives the coefficients of the polynomial
`integerNormalization p` -/
noncomputable def coeffIntegerNormalization (p : S[X]) (i : ℕ) : R :=
if hi : i ∈ p.support then
Classical.choose
(Classical.choose_spec (exist_integer_multiples_of_finset M (p.support.image p.coeff)) (p.coeff i)
(Finset.mem_image.mpr ⟨i, hi, rfl⟩))
else 0
