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

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
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
    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⁻¹)
      source
      theorem IsFractionRing.num_den_unique (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) (n : A) (d : ↥(nonZeroDivisors A)) (pr : IsRelPrime n ↑d) (h : IsLocalization.mk' K n d = x) :
      Associated (num A x) n ∧ Associated ↑(den A x) ↑d
      source
      theorem IsFractionRing.exists_sq_mul_squarefree (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (q : K) :
      ∃ (r : K) (d : A), r ^ 2 * (algebraMap A K) d = q ∧ Squarefree d

      Every element of the fraction field of a unique factorization domain is a square times a squarefree element.