mathlib documentation

ring_theory.coprime.lemmas

Additional lemmas about elements of a ring satisfying is_coprime #

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 is_coprime.prod_left {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
(∀ (i : I), i tis_coprime (s i) x)is_coprime (t.prod (λ (i : I), s i)) x
theorem is_coprime.prod_right {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
(∀ (i : I), i tis_coprime x (s i))is_coprime x (t.prod (λ (i : I), s i))
theorem is_coprime.prod_left_iff {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
is_coprime (t.prod (λ (i : I), s i)) x ∀ (i : I), i tis_coprime (s i) x
theorem is_coprime.prod_right_iff {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
is_coprime x (t.prod (λ (i : I), s i)) ∀ (i : I), i tis_coprime x (s i)
theorem is_coprime.of_prod_left {R : Type u} {I : Type v} [comm_semiring R] {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} [comm_semiring R] {x : R} {s : I → R} {t : finset I} (H1 : is_coprime x (t.prod (λ (i : I), s i))) (i : I) (hit : i t) :
is_coprime x (s i)
theorem finset.prod_dvd_of_coprime {R : Type u} {I : Type v} [comm_semiring R] {z : R} {s : I → R} {t : finset I} (Hs : t.pairwise (is_coprime on s)) (Hs1 : ∀ (i : I), i ts i z) :
t.prod (λ (x : I), s x) z
theorem fintype.prod_dvd_of_coprime {R : Type u} {I : Type v} [comm_semiring R] {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} [comm_semiring R] {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} [comm_semiring R] {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} [comm_semiring R] {s : I → R} {t : finset I} [decidable_eq I] :
pairwise (is_coprime on λ (i : t), s i) ∀ (i : I), i tis_coprime (s i) ((t \ {i}).prod (λ (j : I), s j))
theorem is_coprime.pow_left {R : Type u} [comm_semiring R] {x y : R} {m : } (H : is_coprime x y) :
is_coprime (x ^ m) y
theorem is_coprime.pow_right {R : Type u} [comm_semiring R] {x y : R} {n : } (H : is_coprime x y) :
is_coprime x (y ^ n)
theorem is_coprime.pow {R : Type u} [comm_semiring R] {x y : R} {m n : } (H : is_coprime x y) :
is_coprime (x ^ m) (y ^ n)
theorem is_coprime.pow_left_iff {R : Type u} [comm_semiring R] {x y : R} {m : } (hm : 0 < m) :
theorem is_coprime.pow_right_iff {R : Type u} [comm_semiring R] {x y : R} {m : } (hm : 0 < m) :
theorem is_coprime.pow_iff {R : Type u} [comm_semiring R] {x y : R} {m n : } (hm : 0 < m) (hn : 0 < n) :
is_coprime (x ^ m) (y ^ n) is_coprime x y