Theorems · Theorem · field theory

RatFunc.laurentAux_ofFractionRing_mk

∀ {R : Type u} [inst : CommRing R] (r : R) (p : Polynomial R) (q : ↥(nonZeroDivisors (Polynomial R))),
  (RatFunc.laurentAux r) { toFractionRing := Localization.mk p q } =
    { toFractionRing := Localization.mk ((Polynomial.taylor r) p) ⟨(Polynomial.taylor r) ↑q, ⋯⟩ }

Defined in

Mathlib.FieldTheory.Laurent

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing