mathlib documentation

ring_theory.localization.num_denom

Numerator and denominator in a localization #

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) :
∃ (a : A) (b : (non_zero_divisors A)), (∀ {d : A}, d ad bis_unit d) is_localization.mk' K a b = x
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} :
@[simp]
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