integralNormalization_coeff — Mathlib

English

Coefficient formula for integralNormalization: coeff equals 1 if degree equals index, else coeff times leadCoeff^(natDegree-1-index).

Русский

Формула коэффициентов интегральной нормализации: коэффициент равен 1 при совпадении степени и индекса, иначе — произведение коэффициента и степени ведущего коэффициента.

LaTeX

$$$\text{coeff}_{i}(\text{integralNormalization}(p)) = \begin{cases} 1, & \deg(p) = i; \\ coeff(p,i) \cdot (\text{leadingCoeff}(p))^{\deg(p) - 1 - i}, & \text{иначе}.\end{cases}$$$

Lean4

theorem integralNormalization_coeff {i : ℕ} :
    (integralNormalization p).coeff i =
      if p.degree = i then 1 else coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i) :=
  by
  have : p.coeff i = 0 → p.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc
  simp +contextual [sum_def, integralNormalization, coeff_monomial, this, mem_support_iff]

Похожие утверждения