Mathlib Map

Theorems · Theorem · field theory

RatFunc.mk_def_of_mem

∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K) {q : Polynomial K}
  (hq : q ∈ nonZeroDivisors (Polynomial K)),
  RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p ⟨q, hq⟩ }
Defined in
Mathlib.FieldTheory.RatFunc.Defs
Cited by
1 results in Mathlib
Foundations
Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingIsDomain
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

RatFunc.mk_def_of_ne · cited by 2RatFunc.mk_def_of_neCommRing · cited by 17173CommRingPolynomial · cited by 5681PolynomialSubmonoid · cited by 3086SubmonoidIsDomain · cited by 2196IsDomainnonZeroDivisors · cited by 895nonZeroDivisorsRatFunc · cited by 301RatFuncIsLocalization.mk' · cited by 218IsLocalization.mk'FractionRing · cited by 200FractionRingRatFunc.mk · cited by 21RatFunc.mkRatFunc.mk_def_of_memCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.