integralNormalization_coeff_natDegree

English

If p is a polynomial with p ≠ 0, then the coefficient at natDegree(p) in the integral normalization of p is 1.

Русский

Пусть p не равен нулю; тогда коэффициент при natDegree(p) в нормализации интеграла от p равен 1.

LaTeX

$$$p \neq 0 \Rightarrow \operatorname{coeff}(\operatorname{integralNormalization}(p), \operatorname{natDegree}(p)) = 1$$$

Lean4

theorem integralNormalization_coeff_natDegree (hp : p ≠ 0) : (integralNormalization p).coeff (natDegree p) = 1 :=
  integralNormalization_coeff_degree (degree_eq_natDegree hp)

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