# 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

source
theorem IsFractionRing.exists_reduced_fraction (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a ↑b ∧ IsLocalization.mk' K a b = x
source
noncomputable def IsFractionRing.num (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [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

- IsFractionRing.num A x = Classical.choose ⋯

Instances For

source
noncomputable def IsFractionRing.den (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
↥(nonZeroDivisors A)

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

Equations

- IsFractionRing.den A x = Classical.choose ⋯

Instances For

source
theorem IsFractionRing.num_den_reduced (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
IsRelPrime (num A x) ↑(den A x)
source
theorem IsFractionRing.mk'_num_den (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
IsLocalization.mk' K (num A x) (den A x) = x
source
@[simp]
theorem IsFractionRing.mk'_num_den' (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
(algebraMap A K) (num A x) / (algebraMap A K) ↑(den A x) = x
source
theorem IsFractionRing.num_mul_den_eq_num_iff_eq {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x y : K} :
x * (algebraMap A K) ↑(den A y) = (algebraMap A K) (num A y) ↔ x = y
source
theorem IsFractionRing.num_mul_den_eq_num_iff_eq' {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x y : K} :
y * (algebraMap A K) ↑(den A x) = (algebraMap A K) (num A x) ↔ x = y
source
theorem IsFractionRing.num_mul_den_eq_num_mul_den_iff_eq {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x y : K} :
num A y * ↑(den A x) = num A x * ↑(den A y) ↔ x = y
source
theorem IsFractionRing.eq_zero_of_num_eq_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x : K} (h : num A x = 0) :
x = 0
source
@[simp]
theorem IsFractionRing.num_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] :
num A 0 = 0
source
@[simp]
theorem IsFractionRing.num_eq_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
num A x = 0 ↔ x = 0
source
theorem IsFractionRing.isInteger_of_isUnit_den {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {x : K} (h : IsUnit ↑(den A x)) :
IsLocalization.IsInteger A x
source
theorem IsFractionRing.isUnit_den_iff {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :
IsUnit ↑(den A x) ↔ IsLocalization.IsInteger A x
source
theorem IsFractionRing.isUnit_den_zero {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] :
IsUnit ↑(den A 0)
source
theorem IsFractionRing.associated_den_num_inv {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) (hx : x ≠ 0) :
Associated (↑(den A x)) (num A x⁻¹)
source
theorem IsFractionRing.associated_num_den_inv {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) (hx : x ≠ 0) :
Associated (num A x) ↑(den A x⁻¹)