Theorems · Theorem · field theory

RatFunc.laurent_div

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

Defined in

Mathlib.FieldTheory.Laurent

Cited by

1 results in Mathlib

Foundations

Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain