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
📐 coverage
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
🔸 coverage
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
      🔸 coverage
      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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          @[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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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