English
If q ∈ R[X]⁰, then laurentAux r maps the fraction class of (p/q) (in the fraction field of R[X]) to the fraction of (taylor r p)/(taylor r q).
Русский
Если q ∈ R[X]⁰, то laurentAux r переводит долю p/q в долю taylor r p over taylor r q в поле дробей R[X].
LaTeX
$$$q \\in R[X]^{0} \\Rightarrow \\mathrm{laurentAux}(r)(\\mathrm{ofFractionRing}(\\mathrm{Localization.mk}~p~q)) = \\mathrm{ofFractionRing}(\\mathrm{mk}(\\operatorname{taylor}(r) p) \\langle \\operatorname{taylor}(r) q, \\operatorname{taylor\\_mem\\_nonZeroDivisors} (r) q q.prop\\rangle).$$$
Lean4
theorem laurentAux_ofFractionRing_mk (q : R[X]⁰) :
laurentAux r (ofFractionRing (Localization.mk p q)) =
ofFractionRing (.mk (taylor r p) ⟨taylor r q, taylor_mem_nonZeroDivisors r q q.prop⟩) :=
map_apply_ofFractionRing_mk _ _ _ _
