Theorems · Definition · commutative algebra

IsFractionRing.den

(A : Type u_1) →
  [inst : CommRing A] →
    [IsDomain A] →
      [UniqueFactorizationMonoid A] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra A K] → [IsFractionRing A K] → K → ↥(nonZeroDivisors A)

f.den x is the denominator of x : f.codomain as a reduced fraction.

Defined in

Mathlib.RingTheory.Localization.NumDen

Cited by

22 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainUniqueFactorizationMonoidFieldAlgebraIsFractionRing