integralNormalization_coeff_degree_ne

English

If i is not equal to deg(p), then the i-th coefficient of the integral normalization of p is the original i-th coefficient times the leading coefficient of p raised to the power natDegree(p) - 1 - i.

Русский

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

LaTeX

$$$i \neq \deg(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_degree_ne {i : ℕ} (hi : p.degree ≠ i) :
    coeff (integralNormalization p) i = coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i) := by
  rw [integralNormalization_coeff, if_neg hi]

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