Skip to content

Commit

Permalink
chore(ring_theory/coprime): split out imports into a new file so that…
Browse files Browse the repository at this point in the history 
… `is_coprime` can be used earlier. (#9403)

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Use.20of.20is_coprime.20in.20rat.2Ebasic/near/254942750)
  • Loading branch information
@eric-wieser
eric-wieser committed Oct 1, 2021
1 parent 102ce30 commit 249a015
Show file tree
Hide file tree
Showing 6 changed files with 106 additions and 81 deletions.
2 changes: 2 additions & 0 deletions src/data/polynomial/field_division.lean
View file
Expand Up @@ -6,6 +6,8 @@ Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
import algebra.gcd_monoid.basic
import data.polynomial.derivative
import data.polynomial.ring_division
import data.set.pairwise
import ring_theory.coprime.lemmas
import ring_theory.euclidean_domain

/-!
Expand Down
2 changes: 1 addition & 1 deletion src/number_theory/fermat4.lean
View file
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul van Wamelen
-/
import number_theory.pythagorean_triples
import ring_theory.coprime
import ring_theory.coprime.lemmas

/-!
# Fermat's Last Theorem for the case n = 4
Expand Down
81 changes: 3 additions & 78 deletions src/ring_theory/coprime.lean → src/ring_theory/coprime/basic.lean
View file
Expand Up @@ -3,11 +3,8 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Ken Lee, Chris Hughes
-/
import algebra.big_operators.basic
import data.fintype.basic
import data.int.gcd
import data.set.pairwise
import tactic.ring
import algebra.ring.basic

/-!
# Coprime elements of a ring
Expand All @@ -18,9 +15,10 @@ import tactic.ring
that `a * x + b * y = 1`. Note that elements with no common divisors are not necessarily coprime,
e.g., the multivariate polynomials `x₁` and `x₂` are not coprime.
See also `ring_theory.coprime.lemmas` for further development of coprime elements.
-/

open_locale classical big_operators
open_locale classical

universes u v

Expand All @@ -34,13 +32,6 @@ e.g., the multivariate polynomials `x₁` and `x₂` are not coprime. -/
@[simp] def is_coprime : Prop :=
∃ a b, a * x + b * y = 1

theorem nat.is_coprime_iff_coprime {m n : ℕ} : is_coprime (m : ℤ) n ↔ nat.coprime m n :=
⟨λ ⟨a, b, H⟩, nat.eq_one_of_dvd_one $ int.coe_nat_dvd.1 $ by { rw [int.coe_nat_one, ← H],
exact dvd_add (dvd_mul_of_dvd_right (int.coe_nat_dvd.2 $ nat.gcd_dvd_left m n) _)
(dvd_mul_of_dvd_right (int.coe_nat_dvd.2 $ nat.gcd_dvd_right m n) _) },
λ H, ⟨nat.gcd_a m n, nat.gcd_b m n, by rw [mul_comm _ (m : ℤ), mul_comm _ (n : ℤ),
← nat.gcd_eq_gcd_ab, show _ = _, from H, int.coe_nat_one]⟩⟩

variables {x y z}

theorem is_coprime.symm (H : is_coprime x y) : is_coprime y x :=
Expand Down Expand Up @@ -87,15 +78,6 @@ calc a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z
theorem is_coprime.mul_right (H1 : is_coprime x y) (H2 : is_coprime x z) : is_coprime x (y * z) :=
by { rw is_coprime_comm at H1 H2 ⊢, exact H1.mul_left H2 }

variables {I : Type v} {s : I → R} {t : finset I}

theorem is_coprime.prod_left : (∀ i ∈ t, is_coprime (s i) x) → is_coprime (∏ i in t, s i) x :=
finset.induction_on t (λ _, is_coprime_one_left) $ λ b t hbt ih H,
by { rw finset.prod_insert hbt, rw finset.forall_mem_insert at H, exact H.1.mul_left (ih H.2) }

theorem is_coprime.prod_right : (∀ i ∈ t, is_coprime x (s i)) → is_coprime x (∏ i in t, s i) :=
by simpa only [is_coprime_comm] using is_coprime.prod_left

theorem is_coprime.mul_dvd (H : is_coprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z :=
begin
obtain ⟨a, b, h⟩ := H,
Expand All @@ -107,23 +89,6 @@ begin
exact (mul_dvd_mul_right H1 _).mul_right _ }
end

theorem finset.prod_dvd_of_coprime :
∀ (Hs : set.pairwise_on (↑t : set I) (is_coprime on s)) (Hs1 : ∀ i ∈ t, s i ∣ z),
∏ x in t, s x ∣ z :=
finset.induction_on t (λ _ _, one_dvd z)
begin
intros a r har ih Hs Hs1,
rw finset.prod_insert har,
have aux1 : a ∈ (↑(insert a r) : set I) := finset.mem_insert_self a r,
refine (is_coprime.prod_right $ λ i hir, Hs a aux1 i _ (by { rintro rfl, exact har hir })).mul_dvd
(Hs1 a aux1) (ih (Hs.mono _) $ λ i hi, Hs1 i (finset.mem_insert_of_mem hi)),
{ exact finset.mem_insert_of_mem hir },
{ simp only [finset.coe_insert, set.subset_insert] }
end

theorem fintype.prod_dvd_of_coprime [fintype I] (Hs : pairwise (is_coprime on s))
(Hs1 : ∀ i, s i ∣ z) : ∏ x, s x ∣ z :=
finset.prod_dvd_of_coprime (Hs.pairwise_on _) (λ i _, Hs1 i)

theorem is_coprime.of_mul_left_left (H : is_coprime (x * y) z) : is_coprime x z :=
let ⟨a, b, h⟩ := H in ⟨a * y, b, by rwa [mul_right_comm, mul_assoc]⟩
Expand All @@ -143,46 +108,6 @@ theorem is_coprime.mul_left_iff : is_coprime (x * y) z ↔ is_coprime x z ∧ is
theorem is_coprime.mul_right_iff : is_coprime x (y * z) ↔ is_coprime x y ∧ is_coprime x z :=
by rw [is_coprime_comm, is_coprime.mul_left_iff, is_coprime_comm, @is_coprime_comm _ _ z]

theorem is_coprime.prod_left_iff : is_coprime (∏ i in t, s i) x ↔ ∀ i ∈ t, is_coprime (s i) x :=
finset.induction_on t (iff_of_true is_coprime_one_left $ λ _, false.elim) $ λ b t hbt ih,
by rw [finset.prod_insert hbt, is_coprime.mul_left_iff, ih, finset.forall_mem_insert]

theorem is_coprime.prod_right_iff : is_coprime x (∏ i in t, s i) ↔ ∀ i ∈ t, is_coprime x (s i) :=
by simpa only [is_coprime_comm] using is_coprime.prod_left_iff

theorem is_coprime.of_prod_left (H1 : is_coprime (∏ i in t, s i) x) (i : I) (hit : i ∈ t) :
is_coprime (s i) x :=
is_coprime.prod_left_iff.1 H1 i hit

theorem is_coprime.of_prod_right (H1 : is_coprime x (∏ i in t, s i)) (i : I) (hit : i ∈ t) :
is_coprime x (s i) :=
is_coprime.prod_right_iff.1 H1 i hit

variables {m n : ℕ}

theorem is_coprime.pow_left (H : is_coprime x y) : is_coprime (x ^ m) y :=
by { rw [← finset.card_range m, ← finset.prod_const], exact is_coprime.prod_left (λ _ _, H) }

theorem is_coprime.pow_right (H : is_coprime x y) : is_coprime x (y ^ n) :=
by { rw [← finset.card_range n, ← finset.prod_const], exact is_coprime.prod_right (λ _ _, H) }

theorem is_coprime.pow (H : is_coprime x y) : is_coprime (x ^ m) (y ^ n) :=
H.pow_left.pow_right

theorem is_coprime.pow_left_iff (hm : 0 < m) : is_coprime (x ^ m) y ↔ is_coprime x y :=
begin
refine ⟨λ h, _, is_coprime.pow_left⟩,
rw [← finset.card_range m, ← finset.prod_const] at h,
exact h.of_prod_left 0 (finset.mem_range.mpr hm),
end

theorem is_coprime.pow_right_iff (hm : 0 < m) : is_coprime x (y ^ m) ↔ is_coprime x y :=
is_coprime_comm.trans $ (is_coprime.pow_left_iff hm).trans $ is_coprime_comm

theorem is_coprime.pow_iff (hm : 0 < m) (hn : 0 < n) :
is_coprime (x ^ m) (y ^ n) ↔ is_coprime x y :=
(is_coprime.pow_left_iff hm).trans $ is_coprime.pow_right_iff hn

theorem is_coprime.of_coprime_of_dvd_left (h : is_coprime y z) (hdvd : x ∣ y) : is_coprime x z :=
begin
obtain ⟨d, rfl⟩ := hdvd,
Expand Down
98 changes: 98 additions & 0 deletions src/ring_theory/coprime/lemmas.lean
View file
@@ -0,0 +1,98 @@
/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Ken Lee, Chris Hughes
-/
import algebra.big_operators.basic
import data.fintype.basic
import data.int.gcd
import data.set.pairwise
import ring_theory.coprime.basic

/-!
# 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`.
-/

universes u v

variables {R : Type u} {I : Type v} [comm_semiring R] {x y z : R} {s : I → R} {t : finset I}

open_locale big_operators classical

theorem nat.is_coprime_iff_coprime {m n : ℕ} : is_coprime (m : ℤ) n ↔ nat.coprime m n :=
⟨λ ⟨a, b, H⟩, nat.eq_one_of_dvd_one $ int.coe_nat_dvd.1 $ by { rw [int.coe_nat_one, ← H],
exact dvd_add (dvd_mul_of_dvd_right (int.coe_nat_dvd.2 $ nat.gcd_dvd_left m n) _)
(dvd_mul_of_dvd_right (int.coe_nat_dvd.2 $ nat.gcd_dvd_right m n) _) },
λ H, ⟨nat.gcd_a m n, nat.gcd_b m n, by rw [mul_comm _ (m : ℤ), mul_comm _ (n : ℤ),
← nat.gcd_eq_gcd_ab, show _ = _, from H, int.coe_nat_one]⟩⟩

theorem is_coprime.prod_left : (∀ i ∈ t, is_coprime (s i) x) → is_coprime (∏ i in t, s i) x :=
finset.induction_on t (λ _, is_coprime_one_left) $ λ b t hbt ih H,
by { rw finset.prod_insert hbt, rw finset.forall_mem_insert at H, exact H.1.mul_left (ih H.2) }

theorem is_coprime.prod_right : (∀ i ∈ t, is_coprime x (s i)) → is_coprime x (∏ i in t, s i) :=
by simpa only [is_coprime_comm] using is_coprime.prod_left

theorem is_coprime.prod_left_iff : is_coprime (∏ i in t, s i) x ↔ ∀ i ∈ t, is_coprime (s i) x :=
finset.induction_on t (iff_of_true is_coprime_one_left $ λ _, false.elim) $ λ b t hbt ih,
by rw [finset.prod_insert hbt, is_coprime.mul_left_iff, ih, finset.forall_mem_insert]

theorem is_coprime.prod_right_iff : is_coprime x (∏ i in t, s i) ↔ ∀ i ∈ t, is_coprime x (s i) :=
by simpa only [is_coprime_comm] using is_coprime.prod_left_iff

theorem is_coprime.of_prod_left (H1 : is_coprime (∏ i in t, s i) x) (i : I) (hit : i ∈ t) :
is_coprime (s i) x :=
is_coprime.prod_left_iff.1 H1 i hit

theorem is_coprime.of_prod_right (H1 : is_coprime x (∏ i in t, s i)) (i : I) (hit : i ∈ t) :
is_coprime x (s i) :=
is_coprime.prod_right_iff.1 H1 i hit

theorem finset.prod_dvd_of_coprime :
∀ (Hs : set.pairwise_on (↑t : set I) (is_coprime on s)) (Hs1 : ∀ i ∈ t, s i ∣ z),
∏ x in t, s x ∣ z :=
finset.induction_on t (λ _ _, one_dvd z)
begin
intros a r har ih Hs Hs1,
rw finset.prod_insert har,
have aux1 : a ∈ (↑(insert a r) : set I) := finset.mem_insert_self a r,
refine (is_coprime.prod_right $ λ i hir, Hs a aux1 i _ (by { rintro rfl, exact har hir })).mul_dvd
(Hs1 a aux1) (ih (Hs.mono _) $ λ i hi, Hs1 i (finset.mem_insert_of_mem hi)),
{ exact finset.mem_insert_of_mem hir },
{ simp only [finset.coe_insert, set.subset_insert] }
end

theorem fintype.prod_dvd_of_coprime [fintype I] (Hs : pairwise (is_coprime on s))
(Hs1 : ∀ i, s i ∣ z) : ∏ x, s x ∣ z :=
finset.prod_dvd_of_coprime (Hs.pairwise_on _) (λ i _, Hs1 i)

variables {m n : ℕ}

theorem is_coprime.pow_left (H : is_coprime x y) : is_coprime (x ^ m) y :=
by { rw [← finset.card_range m, ← finset.prod_const], exact is_coprime.prod_left (λ _ _, H) }

theorem is_coprime.pow_right (H : is_coprime x y) : is_coprime x (y ^ n) :=
by { rw [← finset.card_range n, ← finset.prod_const], exact is_coprime.prod_right (λ _ _, H) }

theorem is_coprime.pow (H : is_coprime x y) : is_coprime (x ^ m) (y ^ n) :=
H.pow_left.pow_right

theorem is_coprime.pow_left_iff (hm : 0 < m) : is_coprime (x ^ m) y ↔ is_coprime x y :=
begin
refine ⟨λ h, _, is_coprime.pow_left⟩,
rw [← finset.card_range m, ← finset.prod_const] at h,
exact h.of_prod_left 0 (finset.mem_range.mpr hm),
end

theorem is_coprime.pow_right_iff (hm : 0 < m) : is_coprime x (y ^ m) ↔ is_coprime x y :=
is_coprime_comm.trans $ (is_coprime.pow_left_iff hm).trans $ is_coprime_comm

theorem is_coprime.pow_iff (hm : 0 < m) (hn : 0 < n) :
is_coprime (x ^ m) (y ^ n) ↔ is_coprime x y :=
(is_coprime.pow_left_iff hm).trans $ is_coprime.pow_right_iff hn
2 changes: 1 addition & 1 deletion src/ring_theory/euclidean_domain.lean
View file
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Chris Hughes
-/
import ring_theory.coprime
import ring_theory.coprime.basic
import ring_theory.ideal.basic

/-!
Expand Down
2 changes: 1 addition & 1 deletion src/ring_theory/int/basic.lean
View file
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Jens Wagemaker, Aaron Anderson
-/
import ring_theory.coprime
import ring_theory.coprime.basic
import ring_theory.unique_factorization_domain

/-!
Expand Down

0 comments on commit 249a015

Please sign in to comment.