integralNormalization_coeff_degree

English

Let p be a polynomial. If the degree of p equals i, then the i-th coefficient of the integral normalization of p is 1.

Русский

Пусть p — многочлен. Если deg(p) = i, то i-й коэффициент нормализации интеграла от p равен 1.

LaTeX

$$$\deg(p) = i \Rightarrow \operatorname{coeff}(\operatorname{integralNormalization}(p), i) = 1$$$

Lean4

theorem integralNormalization_coeff_degree {i : ℕ} (hi : p.degree = i) : (integralNormalization p).coeff i = 1 := by
  rw [integralNormalization_coeff, if_pos hi]

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