Numerator and denominator in a localization #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Implementation notes #
See src/ring_theory/localization/basic.lean for a design overview.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
theorem
is_fraction_ring.exists_reduced_fraction
(A : Type u_4)
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
(x : K) :
noncomputable
def
is_fraction_ring.num
(A : Type u_4)
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
(x : K) :
A
f.num x is the numerator of x : f.codomain as a reduced fraction.
Equations
noncomputable
def
is_fraction_ring.denom
(A : Type u_4)
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
(x : K) :
f.num x is the denominator of x : f.codomain as a reduced fraction.
Equations
theorem
is_fraction_ring.num_denom_reduced
(A : Type u_4)
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
(x : K)
{d : A} :
d ∣ is_fraction_ring.num A x → d ∣ ↑(is_fraction_ring.denom A x) → is_unit d
@[simp]
theorem
is_fraction_ring.mk'_num_denom
(A : Type u_4)
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
(x : K) :
is_localization.mk' K (is_fraction_ring.num A x) (is_fraction_ring.denom A x) = x
theorem
is_fraction_ring.num_mul_denom_eq_num_iff_eq
{A : Type u_4}
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
{x y : K} :
x * ⇑(algebra_map A K) ↑(is_fraction_ring.denom A y) = ⇑(algebra_map A K) (is_fraction_ring.num A y) ↔ x = y
theorem
is_fraction_ring.num_mul_denom_eq_num_iff_eq'
{A : Type u_4}
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
{x y : K} :
y * ⇑(algebra_map A K) ↑(is_fraction_ring.denom A x) = ⇑(algebra_map A K) (is_fraction_ring.num A x) ↔ x = y
theorem
is_fraction_ring.num_mul_denom_eq_num_mul_denom_iff_eq
{A : Type u_4}
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
{x y : K} :
is_fraction_ring.num A y * ↑(is_fraction_ring.denom A x) = is_fraction_ring.num A x * ↑(is_fraction_ring.denom A y) ↔ x = y
theorem
is_fraction_ring.eq_zero_of_num_eq_zero
{A : Type u_4}
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
{x : K}
(h : is_fraction_ring.num A x = 0) :
x = 0
theorem
is_fraction_ring.is_integer_of_is_unit_denom
{A : Type u_4}
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
{x : K}
(h : is_unit ↑(is_fraction_ring.denom A x)) :
theorem
is_fraction_ring.is_unit_denom_of_num_eq_zero
{A : Type u_4}
[comm_ring A]
[is_domain A]
[unique_factorization_monoid A]
{K : Type u_5}
[field K]
[algebra A K]
[is_fraction_ring A K]
{x : K}
(h : is_fraction_ring.num A x = 0) :