monic_integralNormalization — Mathlib

English

If p ≠ 0, then integralNormalization(p) is monic.

Русский

Если p ≠ 0, то интегральная нормализация от p является монической (мономодной единице).

LaTeX

$$$p \neq 0 \Rightarrow \operatorname{Monic}(\operatorname{integralNormalization}(p))$$$

Lean4

theorem monic_integralNormalization (hp : p ≠ 0) : Monic (integralNormalization p) :=
  monic_of_degree_le p.natDegree
    (Finset.sup_le fun i h =>
      WithBot.coe_le_coe.2 <| le_natDegree_of_mem_supp i <| support_integralNormalization_subset h)
    (integralNormalization_coeff_natDegree hp)

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