English
There exists a Laurent auxiliary endomorphism laurentAux on RatFunc R obtained by applying the Taylor map on the polynomial variable, well-defined by the nonZeroDivisors preservation.
Русский
Существует расщепляющее дополнение Лаурентова типа на RatFunc R, задающееся применением отображения Тейлора на многочленах; существование обеспечивается сохранением ненулевых делителей.
LaTeX
$$$\\mathrm{laurentAux} : \\operatorname{RatFunc} R \\to^+ \\operatorname{RatFunc} R \\quad \\text{is defined by } \\mathrm{laurentAux} = \\mathrm{RatFunc.mapRingHom}(\\varphi)\\text{ with } \\varphi = \\operatorname{taylor}(r) \\text{ and } \\operatorname{taylor\\_mem\\_nonZeroDivisors}(r).$$$
Lean4
/-- The Laurent expansion of rational functions about a value.
Auxiliary definition, usage when over integral domains should prefer `RatFunc.laurent`. -/
def laurentAux : RatFunc R →+* RatFunc R :=
RatFunc.mapRingHom
({ toFun := taylor r
map_add' := map_add (taylor r)
map_mul' := taylor_mul _
map_zero' := map_zero (taylor r)
map_one' := taylor_one r } : R[X] →+* R[X]) (taylor_mem_nonZeroDivisors _)
