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 ∈ t → is_coprime (s i) x) → is_coprime (∏ (i : I) in t, 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 (∏ (i : I) in t, 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 (∏ (i : I) in t, 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 (∏ (i : I) in t, 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 (∏ (i : I) in t, 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 (∏ (i : I) in t, 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) :
∏ (x : I) in t, 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) :
∏ (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}
(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] :
theorem
pairwise_coprime_iff_coprime_prod
{R : Type u}
{I : Type v}
[comm_semiring R]
{s : I → R}
{t : finset I} :
pairwise (is_coprime on λ (i : ↥t), s ↑i) ↔ ∀ (i : I), i ∈ t → is_coprime (s i) (∏ (j : I) in t \ {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