Theorems · Theorem · field theory

RatFunc.mk_def_of_ne

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

Defined in

Mathlib.FieldTheory.RatFunc.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain