English
For power series f,g over a local ring A, define the Weierstrass quotient f /ʷ g as the corresponding quotient in the division process; if the image of g in the residue field is zero, this quotient is defined to be zero.
Русский
Для степенной серии f и g над локальным кольцом A определим квотиент по Вайершрасу f /ʷ g как соответствующий квотиент в процессе деления; если образ g в резидуальном поле равен нулю, квотиент равен нулю.
LaTeX
$$$f /\!\stard b g \text{ is defined as the Weierstrass quotient, with } f /ʷ g = 0 \text{ if } g\mapsto 0 \text{ in the residue field}$$$
Lean4
/-- The quotient `q` 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 weierstrassDiv [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).div f else 0
