integralNormalization_coeff_ne_natDegree

English

If i ≠ natDegree(p), then the i-th coefficient of the integral normalization of p is coeff(p,i) times leadingCoeff(p)^{natDegree(p) - 1 - i}.

Русский

Если i ≠ natDegree(p), то i-й коэффициент интегральной нормализации равен coeff(p,i) · leadCoeff(p)^{natDegree(p) - 1 - i}.

LaTeX

$$$i \neq \operatorname{natDegree}(p) \Rightarrow \operatorname{coeff}(\operatorname{integralNormalization}(p), i) = \operatorname{coeff}(p,i) \cdot (\operatorname{leadingCoeff}(p))^{(\operatorname{natDegree}(p) - 1 - i)}$$$

Lean4

theorem integralNormalization_coeff_ne_natDegree {i : ℕ} (hi : i ≠ natDegree p) :
    coeff (integralNormalization p) i = coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i) :=
  integralNormalization_coeff_degree_ne (degree_ne_of_natDegree_ne hi.symm)

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