English
For power series f,g over a local ring A, the Weierstrass remainder f %ʷ g is defined; it is zero if the residue of g is zero, otherwise it is the remainder upon division.
Русский
Для степенной серии f и g над локальным кольцом A оста́ток по Вайершрасу f %ʷ g задан; если образ g в остаточном поле равен нулю, остаток равен нулю; иначе — остаток деления.
LaTeX
$$$f \%\!\wp g \in A[X],\quad \text{and } f = g q + r \text{ with } r = f \%\!\wp g$$$
Lean4
/-- The remainder `r` in Weierstrass division, denoted by `f %ʷ g`. Note that when the image of
`g` in the residue field is zero, this is defined to be zero. -/
noncomputable def weierstrassMod [IsPrecomplete (IsLocalRing.maximalIdeal A) A] : A[X] :=
open scoped Classical in
if hg : g.map (IsLocalRing.residue A) ≠ 0 then (IsWeierstrassDivisor.of_map_ne_zero hg).mod f else 0
