IsFractionRing.exists_reduced_fraction
theorem IsFractionRing.exists_reduced_fraction :
∀ (A : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_5}
[inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
∃ a b, IsRelPrime a ↑b ∧ IsLocalization.mk' K a b = x
The theorem `IsFractionRing.exists_reduced_fraction` states that for every element `x` in the field of fractions `K` of an integral domain `A` (with `A` possessing the structure of a commutative ring, an integral domain, and a unique factorization monoid), there exists a pair of elements `a` and `b` such that `a` and `b` are relatively prime (i.e., any common divisor of `a` and `b` is a unit) and the fraction `a/b` represented by the localization map equals `x`. In other words, every element of the field of fractions can be represented as a fraction of two relatively prime elements from the integral domain.
More concisely: For every element in the field of fractions of a commutative ring that is an integral domain and a unique factorization monoid, there exists a pair of relatively prime elements whose localization gives that element.
|
IsFractionRing.mk'_num_den
theorem IsFractionRing.mk'_num_den :
∀ (A : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_5}
[inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
IsLocalization.mk' K (IsFractionRing.num A x) (IsFractionRing.den A x) = x
The theorem `IsFractionRing.mk'_num_den` states that for any type `A` which is a commutative ring, an integral domain, and a unique factorization monoid, and any field `K` which is an algebra over `A` and also the field of fractions of `A`, for any element `x` of `K`, applying the function `IsLocalization.mk'` to the numerator (`IsFractionRing.num A x`) and the denominator (`IsFractionRing.den A x`) of `x` will yield `x` itself. In other words, every element of the field `K` can be expressed as the fraction of its numerator and denominator, where the fraction is constructed by `IsLocalization.mk'`.
More concisely: For any commutative ring A that is an integral domain and a unique factorization monoid, andany field K that is an algebra over A and the field of fractions of A, the application of `IsLocalization.mk'` to the numerator and denominator of any element x in K yields x itself.
|