# mathlib3documentation

ring_theory.localization.integer

# Integer elements of 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

def is_localization.is_integer (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] (a : S) :
Prop

Given a : S, S a localization of R, is_integer R a iff a is in the image of the localization map from R to S.

Equations
theorem is_localization.is_integer_zero {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] :
theorem is_localization.is_integer_one {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] :
theorem is_localization.is_integer_add {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a b : S} (ha : a) (hb : b) :
(a + b)
theorem is_localization.is_integer_mul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a b : S} (ha : a) (hb : b) :
(a * b)
theorem is_localization.is_integer_smul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a : R} {b : S} (hb : b) :
(a b)
theorem is_localization.exists_integer_multiple' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (a : S) :
(b : M), (a * S) b)

Each element a : S has an M-multiple which is an integer.

This version multiplies a on the right, matching the argument order in localization_map.surj.

theorem is_localization.exists_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (a : S) :
(b : M), (b a)

Each element a : S has an M-multiple which is an integer.

This version multiplies a on the left, matching the argument order in the has_smul instance.

theorem is_localization.exist_integer_multiples {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι S) :
(b : M), (i : ι), i s (b f i)

We can clear the denominators of a finset-indexed family of fractions.

theorem is_localization.exist_integer_multiples_of_finite {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} [finite ι] (f : ι S) :
(b : M), (i : ι), (b f i)

We can clear the denominators of a finite indexed family of fractions.

theorem is_localization.exist_integer_multiples_of_finset {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (s : finset S) :
(b : M), (a : S), a s (b a)

We can clear the denominators of a finite set of fractions.

noncomputable def is_localization.common_denom {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι S) :

A choice of a common multiple of the denominators of a finset-indexed family of fractions.

Equations
noncomputable def is_localization.integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι S) (i : s) :
R

The numerator of a fraction after clearing the denominators of a finset-indexed family of fractions.

Equations
@[simp]
theorem is_localization.map_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι S) (i : s) :
S) i) = f i
noncomputable def is_localization.common_denom_of_finset {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (s : finset S) :

A choice of a common multiple of the denominators of a finite set of fractions.

Equations
noncomputable def is_localization.finset_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] [decidable_eq R] (s : finset S) :

The finset of numerators after clearing the denominators of a finite set of fractions.

Equations
theorem is_localization.finset_integer_multiple_image {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] [decidable_eq R] (s : finset S) :