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

source
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 : ↥A⁰), (∀ {d : A}, d ∣ a → d ∣ ↑b → is_unit d) ∧ is_localization.mk' K a b = x
source
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
source
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) :
↥A⁰

f.num x is the denominator of x : f.codomain as a reduced fraction.

Equations
source
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
source
@[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
source
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
source
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
source
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
source
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
source
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)) :
is_localization.is_integer A x
source
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) :
is_unit ↑(is_fraction_ring.denom A x)