Theorems · Theorem · field theory

RatFunc.mk_eq_localization_mk

∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0),
  RatFunc.mk p q = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }

Defined in

Mathlib.FieldTheory.RatFunc.Defs

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain