RatFunc.laurent_algebraMap

theorem RatFunc.laurent_algebraMap : ∀ {R : Type u} [inst : CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R), (RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)

This theorem states that for any commutative ring `R` which is also an integral domain, given a value `r` in `R` and a polynomial `p` with coefficients in `R`, applying the Laurent expansion of rational functions to the result of embedding the polynomial into the field of rational functions over `R` (via the algebra map) is equivalent to first applying the Taylor expansion of the polynomial at `r` and then embedding the result into the field of rational functions.

More concisely: For any commutative ring `R` that is an integral domain, the Laurent expansion of the rational function obtained from embedding a polynomial `p` in `R` into the field of rational functions over `R`, is equivalent to first performing the Taylor expansion of `p` at `r` and then embedding the result into the field of rational functions.