Theorems · Definition · commutative algebra

IsFractionRing.num

(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 → A

f.num x is the numerator of x : f.codomain as a reduced fraction.

Defined in

Mathlib.RingTheory.Localization.NumDen

Cited by

22 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainUniqueFactorizationMonoidFieldAlgebraIsFractionRing