weierstrassDistinguished — Mathlib

English

The distinguished polynomial in the Weierstrass factorization is the chosen representative f that captures the divisor part of g.

Русский

Отличительная часть факторизации — это выбранный многочлен f, задающий раздел делителя g.

LaTeX

$$$f = \text{distinguished part of } g$$$

Lean4

/-- The `f` in the Weierstrass preparation theorem. -/
noncomputable def weierstrassDistinguished (hg : g.map (IsLocalRing.residue A) ≠ 0) : A[X] :=
  (g.exists_isWeierstrassFactorization hg).choose

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