English
There is an R-algebra endomorphism laurent r of RatFunc R, defined by applying the Taylor map on the underlying polynomial data.
Русский
Существует R-алгебраический эндоморфизм laurent r над RatFunc R, задаваемый применением отображения Тейлора к базовым полиномам.
LaTeX
$$$ laurent r : \\operatorname{RatFunc} R \\to_{\\!R} \\operatorname{RatFunc} R \\quad \\text{is an algebra homomorphism defined by} \\quad laurent r = \\mathrm{RatFunc.mapAlgHom}(\\mathrm{ofLinearMap}(\\operatorname{taylor}(r))(\\operatorname{taylor\_one})(\\operatorname{taylor\_mul})).$$$
Lean4
/-- The Laurent expansion of rational functions about a value. -/
def laurent : RatFunc R →ₐ[R] RatFunc R :=
RatFunc.mapAlgHom (.ofLinearMap (taylor r) (taylor_one _) (taylor_mul _)) (taylor_mem_nonZeroDivisors _)
