English
For r ∈ R and p,q ∈ R[X], with q non-zero-divisor, laurent r maps the fraction p/q to the fraction taylor r p / taylor r q in RatFunc R.
Русский
Для r ∈ R и p,q ∈ R[X] с q ∈ NZD, laurent r переводит дробь p/q в дробь taylor r p / taylor r q в RatFunc R.
LaTeX
$$$\\forall p,q \\in R[X],\\ q \\in R[X]^{0} \\Rightarrow \\mathrm{laurent}\\_r(\\frac{\\text{algebraMap}(p)}{\\text{algebraMap}(q)}) = \\frac{\\text{algebraMap}(\\operatorname{taylor}(r)p)}{\\text{algebraMap}(\\operatorname{taylor}(r)q)}.$$$
Lean4
theorem laurent_div :
laurent r (algebraMap _ _ p / algebraMap _ _ q) = algebraMap _ _ (taylor r p) / algebraMap _ _ (taylor r q) :=
laurentAux_div r p q
