# mathlib3documentation

ring_theory.coprime.lemmas

# Additional lemmas about elements of a ring satisfying is_coprime#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

These lemmas are in a separate file to the definition of is_coprime as they require more imports.

Notably, this includes lemmas about finset.prod as this requires importing big_operators, and lemmas about has_pow since these are easiest to prove via finset.prod.

theorem nat.coprime.is_coprime {m n : } :

Alias of the reverse direction of nat.is_coprime_iff_coprime.

theorem is_coprime.nat_coprime {m n : } :

Alias of the forward direction of nat.is_coprime_iff_coprime.

theorem is_coprime.prod_left {R : Type u} {I : Type v} {x : R} {s : I R} {t : finset I} :
( (i : I), i t is_coprime (s i) x) is_coprime (t.prod (λ (i : I), s i)) x
theorem is_coprime.prod_right {R : Type u} {I : Type v} {x : R} {s : I R} {t : finset I} :
( (i : I), i t (s i)) (t.prod (λ (i : I), s i))
theorem is_coprime.prod_left_iff {R : Type u} {I : Type v} {x : R} {s : I R} {t : finset I} :
is_coprime (t.prod (λ (i : I), s i)) x (i : I), i t is_coprime (s i) x
theorem is_coprime.prod_right_iff {R : Type u} {I : Type v} {x : R} {s : I R} {t : finset I} :
(t.prod (λ (i : I), s i)) (i : I), i t (s i)
theorem is_coprime.of_prod_left {R : Type u} {I : Type v} {x : R} {s : I R} {t : finset I} (H1 : is_coprime (t.prod (λ (i : I), s i)) x) (i : I) (hit : i t) :
is_coprime (s i) x
theorem is_coprime.of_prod_right {R : Type u} {I : Type v} {x : R} {s : I R} {t : finset I} (H1 : (t.prod (λ (i : I), s i))) (i : I) (hit : i t) :
(s i)
theorem finset.prod_dvd_of_coprime {R : Type u} {I : Type v} {z : R} {s : I R} {t : finset I} (Hs : t.pairwise (is_coprime on s)) (Hs1 : (i : I), i t s i z) :
t.prod (λ (x : I), s x) z
theorem fintype.prod_dvd_of_coprime {R : Type u} {I : Type v} {z : R} {s : I R} [fintype I] (Hs : pairwise (is_coprime on s)) (Hs1 : (i : I), s i z) :
finset.univ.prod (λ (x : I), s x) z
theorem exists_sum_eq_one_iff_pairwise_coprime {R : Type u} {I : Type v} {s : I R} {t : finset I} [decidable_eq I] (h : t.nonempty) :
( (μ : I R), t.sum (λ (i : I), μ i * (t \ {i}).prod (λ (j : I), s j)) = 1) pairwise (is_coprime on λ (i : t), s i)
theorem exists_sum_eq_one_iff_pairwise_coprime' {R : Type u} {I : Type v} {s : I R} [fintype I] [nonempty I] [decidable_eq I] :
( (μ : I R), finset.univ.sum (λ (i : I), μ i * {i}.prod (λ (j : I), s j)) = 1) pairwise (is_coprime on s)
theorem pairwise_coprime_iff_coprime_prod {R : Type u} {I : Type v} {s : I R} {t : finset I} [decidable_eq I] :
pairwise (is_coprime on λ (i : t), s i) (i : I), i t is_coprime (s i) ((t \ {i}).prod (λ (j : I), s j))
theorem is_coprime.pow_left {R : Type u} {x y : R} {m : } (H : y) :
is_coprime (x ^ m) y
theorem is_coprime.pow_right {R : Type u} {x y : R} {n : } (H : y) :
(y ^ n)
theorem is_coprime.pow {R : Type u} {x y : R} {m n : } (H : y) :
is_coprime (x ^ m) (y ^ n)
theorem is_coprime.pow_left_iff {R : Type u} {x y : R} {m : } (hm : 0 < m) :
is_coprime (x ^ m) y y
theorem is_coprime.pow_right_iff {R : Type u} {x y : R} {m : } (hm : 0 < m) :
(y ^ m) y
theorem is_coprime.pow_iff {R : Type u} {x y : R} {m n : } (hm : 0 < m) (hn : 0 < n) :
is_coprime (x ^ m) (y ^ n) y