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_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
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.
Instances For
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.
Instances For
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)
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
@[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
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
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
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}
:
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
@[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
@[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
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))
:
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
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]
:
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⁻¹)
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⁻¹)
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