algEquivQuotientWeierstrassDistinguished

English

There is a canonical A-algebra isomorphism between the polynomial quotient by the distinguished part and the power-series quotient by g.

Русский

Существует канонический A-алгебраический изоморфизм между многочленным делением по отличительной части и делением по g.

LaTeX

$$$A[X]/(f) \cong_A A[[X]]/(g)$$$

Lean4

/-- If `g` is a power series over a complete local ring,
such that its image in the residue field is not zero, then there is a natural isomorphism
`A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g)` where `f` is `PowerSeries.weierstrassDistinguished g`. -/
noncomputable abbrev algEquivQuotientWeierstrassDistinguished (hg : g.map (IsLocalRing.residue A) ≠ 0) :=
  (g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg).algEquivQuotient

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