English
For p,q ∈ R[X] with q a non-zero-divisor, laurentAux r maps algebraMap(p)/algebraMap(q) to algebraMap(taylor r p)/algebraMap(taylor r q).
Русский
Для p,q ∈ R[X] с тем, что q не является нулевым делителем, laurentAux r переводит algebraMap(p)/algebraMap(q) в algebraMap(taylor r p)/algebraMap(taylor r q).
LaTeX
$$$p,q \\in R[X],\\ q \\in R[X]^{0} \\Rightarrow \\mathrm{laurentAux}(r)(\\frac{\\text{algebraMap}(p)}{\\text{algebraMap}(q)}) = \\frac{\\text{algebraMap}(\\operatorname{taylor}(r)p)}{\\text{algebraMap}(\\operatorname{taylor}(r)q)}.$$$
Lean4
theorem laurentAux_div :
laurentAux r (algebraMap _ _ p / algebraMap _ _ q) = algebraMap _ _ (taylor r p) / algebraMap _ _ (taylor r q) :=
-- Porting note: added `by exact taylor_mem_nonZeroDivisors r`
map_apply_div _ (by exact taylor_mem_nonZeroDivisors r) _ _
