Documentation

Mathlib.RingTheory.Localization.NumDen

Numerator and denominator in a localization #

Implementation notes #

See Mathlib/RingTheory/Localization/Basic.lean for a design overview.

Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

theorem IsFractionRing.exists_reduced_fraction (A : Type u_4) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
∃ (a : A) (b : (nonZeroDivisors A)), IsRelPrime a b IsLocalization.mk' K a b = x
noncomputable def IsFractionRing.num (A : Type u_4) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
A

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

Equations
Instances For
    noncomputable def IsFractionRing.den (A : Type u_4) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :

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

    Equations
    Instances For
      @[simp]
      theorem IsFractionRing.mk'_num_den' (A : Type u_4) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
      theorem IsFractionRing.num_mul_den_eq_num_iff_eq {A : Type u_4} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {x : K} {y : K} :
      theorem IsFractionRing.eq_zero_of_num_eq_zero {A : Type u_4} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {x : K} (h : IsFractionRing.num A x = 0) :
      x = 0
      @[simp]
      theorem IsFractionRing.num_eq_zero {A : Type u_4} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
      @[deprecated IsFractionRing.isUnit_den_zero]