Theorems · Theorem · field theory

RatFunc.laurentAux_div

∀ {R : Type u} [inst : CommRing R] (r : R) (p q : Polynomial R) [inst_1 : IsDomain R],
  (RatFunc.laurentAux 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

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain