# 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) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) :
a b, (∀ {d : A}, d ad b) = x
noncomputable def IsFractionRing.num (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) :
A

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

Instances For
noncomputable def IsFractionRing.den (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) :
{ x // }

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

Instances For
theorem IsFractionRing.num_den_reduced (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) {d : A} :
d d ↑()
theorem IsFractionRing.mk'_num_den (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) :
@[simp]
theorem IsFractionRing.mk'_num_den' (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) :
↑() () / ↑() ↑() = x
theorem IsFractionRing.num_mul_den_eq_num_iff_eq {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {x : K} {y : K} :
x * ↑() ↑() = ↑() () x = y
theorem IsFractionRing.num_mul_den_eq_num_iff_eq' {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {x : K} {y : K} :
y * ↑() ↑() = ↑() () x = y
theorem IsFractionRing.num_mul_den_eq_num_mul_den_iff_eq {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {x : K} {y : K} :
* ↑() = * ↑() x = y
theorem IsFractionRing.eq_zero_of_num_eq_zero {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {x : K} (h : = 0) :
x = 0
theorem IsFractionRing.isInteger_of_isUnit_den {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {x : K} (h : IsUnit ↑()) :
theorem IsFractionRing.isUnit_den_of_num_eq_zero {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {x : K} (h : = 0) :
IsUnit ↑()