mathlib3 documentation

ring_theory.localization.num_denom

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) :
(a : A) (b : (non_zero_divisors A)), ( {d : A}, d a d b is_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