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 : A) (b : ()), IsRelPrime a 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.

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

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

Equations
Instances For
theorem IsFractionRing.num_den_reduced (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) :
IsRelPrime () ()
theorem IsFractionRing.mk'_num_den (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) :
= x
@[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 ()