isDistinguishedAt_weierstrassDistinguished

English

The distinguished polynomial associated to g remains distinguished after evaluation at the maximal ideal locus.

Русский

Отличительная часть, связанная с g, сохраняет признак distinguished при локальном рассмотрении.

LaTeX

$$$(g^{\text{dist}}) \;\text{IsDistinguishedAt}\; \mathfrak{m}$$

Lean4

theorem isDistinguishedAt_weierstrassDistinguished (hg : g.map (IsLocalRing.residue A) ≠ 0) :
    (g.weierstrassDistinguished hg).IsDistinguishedAt (IsLocalRing.maximalIdeal A) :=
  (g.exists_isWeierstrassFactorization hg).choose_spec.choose_spec.isDistinguishedAt

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