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.
Alias of the reverse direction of nat.is_coprime_iff_coprime.
Alias of the forward direction of nat.is_coprime_iff_coprime.
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 ∈ 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}
[comm_semiring R]
{x : R}
{s : I → R}
{t : finset I} :
(∀ (i : I), i ∈ t → is_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 ∈ t → is_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 ∈ t → is_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 ∈ t → s i ∣ 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) :
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] :
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 ∈ t → is_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) :
is_coprime (x ^ m) y ↔ is_coprime x y
theorem
is_coprime.pow_right_iff
{R : Type u}
[comm_semiring R]
{x y : R}
{m : ℕ}
(hm : 0 < m) :
is_coprime x (y ^ m) ↔ is_coprime x y
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