From f8741cbc7c2f35d46b8e34add15e52c56c43f45d Mon Sep 17 00:00:00 2001
From: Jeremy Tan Jie Rui <e0191785@u.nus.edu>
Date: Tue, 28 Mar 2023 10:53:25 +0000
Subject: [PATCH] feat: port Algebra.GCDMonoid.Div (#3143)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
---
 Mathlib.lean                       |   1 +
 Mathlib/Algebra/GCDMonoid/Div.lean | 101 +++++++++++++++++++++++++++++
 2 files changed, 102 insertions(+)
 create mode 100644 Mathlib/Algebra/GCDMonoid/Div.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 0dfb8ef0bfb15..2d0d05fb314ee 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -65,6 +65,7 @@ import Mathlib.Algebra.FreeMonoid.Basic
 import Mathlib.Algebra.FreeMonoid.Count
 import Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
 import Mathlib.Algebra.GCDMonoid.Basic
+import Mathlib.Algebra.GCDMonoid.Div
 import Mathlib.Algebra.GCDMonoid.Finset
 import Mathlib.Algebra.GCDMonoid.Multiset
 import Mathlib.Algebra.GeomSum
diff --git a/Mathlib/Algebra/GCDMonoid/Div.lean b/Mathlib/Algebra/GCDMonoid/Div.lean
new file mode 100644
index 0000000000000..6609ad4ba33a9
--- /dev/null
+++ b/Mathlib/Algebra/GCDMonoid/Div.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2022 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+
+! This file was ported from Lean 3 source module algebra.gcd_monoid.div
+! leanprover-community/mathlib commit b537794f8409bc9598febb79cd510b1df5f4539d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.GCDMonoid.Finset
+import Mathlib.Algebra.GCDMonoid.Basic
+import Mathlib.RingTheory.Int.Basic
+import Mathlib.RingTheory.Polynomial.Content
+
+/-!
+# Basic results about setwise gcds on normalized gcd monoid with a division.
+
+## Main results
+
+* `Finset.Nat.gcd_div_eq_one`: given a nonempty Finset `s` and a function `f` from `s` to
+  `ℕ`, if `d = s.gcd`, then the `gcd` of `(f i) / d` equals `1`.
+* `Finset.Int.gcd_div_eq_one`: given a nonempty Finset `s` and a function `f` from `s` to
+  `ℤ`, if `d = s.gcd`, then the `gcd` of `(f i) / d` equals `1`.
+* `Finset.Polynomial.gcd_div_eq_one`: given a nonempty Finset `s` and a function `f` from
+  `s` to `K[X]`, if `d = s.gcd`, then the `gcd` of `(f i) / d` equals `1`.
+
+## TODO
+Add a typeclass to state these results uniformly.
+
+-/
+
+
+namespace Finset
+
+namespace Nat
+
+/-- Given a nonempty Finset `s` and a function `f` from `s` to `ℕ`, if `d = s.gcd`,
+then the `gcd` of `(f i) / d` is equal to `1`. -/
+theorem gcd_div_eq_one {β : Type _} {f : β → ℕ} (s : Finset β) {x : β} (hx : x ∈ s)
+    (hfz : f x ≠ 0) : (s.gcd fun b => f b / s.gcd f) = 1 := by
+  obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
+  refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
+  rw [he a ha, Nat.mul_div_cancel_left]
+  exact Nat.pos_of_ne_zero (mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx)
+#align finset.nat.gcd_div_eq_one Finset.Nat.gcd_div_eq_one
+
+theorem gcd_div_id_eq_one {s : Finset ℕ} {x : ℕ} (hx : x ∈ s) (hnz : x ≠ 0) :
+    (s.gcd fun b => b / s.gcd id) = 1 :=
+  gcd_div_eq_one s hx hnz
+#align finset.nat.gcd_div_id_eq_one Finset.Nat.gcd_div_id_eq_one
+
+end Nat
+
+namespace Int
+
+/-- Given a nonempty Finset `s` and a function `f` from `s` to `ℤ`, if `d = s.gcd`,
+then the `gcd` of `(f i) / d` is equal to `1`. -/
+theorem gcd_div_eq_one {β : Type _} {f : β → ℤ} (s : Finset β) {x : β} (hx : x ∈ s)
+    (hfz : f x ≠ 0) : (s.gcd fun b => f b / s.gcd f) = 1 := by
+  obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
+  refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
+  rw [he a ha, Int.mul_ediv_cancel_left]
+  exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx
+#align finset.int.gcd_div_eq_one Finset.Int.gcd_div_eq_one
+
+theorem gcd_div_id_eq_one {s : Finset ℤ} {x : ℤ} (hx : x ∈ s) (hnz : x ≠ 0) :
+    (s.gcd fun b => b / s.gcd id) = 1 :=
+  gcd_div_eq_one s hx hnz
+#align finset.int.gcd_div_id_eq_one Finset.Int.gcd_div_id_eq_one
+
+end Int
+
+namespace Polynomial
+
+open Polynomial Classical
+
+noncomputable section
+
+variable {K : Type _} [Field K]
+
+/-- Given a nonempty Finset `s` and a function `f` from `s` to `K[X]`, if `d = s.gcd f`,
+then the `gcd` of `(f i) / d` is equal to `1`. -/
+theorem gcd_div_eq_one {β : Type _} {f : β → Polynomial K} (s : Finset β) {x : β} (hx : x ∈ s)
+    (hfz : f x ≠ 0) : (s.gcd fun b => f b / s.gcd f) = 1 := by
+  obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
+  refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
+  rw [he a ha, EuclideanDomain.mul_div_cancel_left]
+  exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx
+#align finset.polynomial.gcd_div_eq_one Finset.Polynomial.gcd_div_eq_one
+
+theorem gcd_div_id_eq_one {s : Finset (Polynomial K)} {x : Polynomial K}
+    (hx : x ∈ s) (hnz : x ≠ 0) : (s.gcd fun b => b / s.gcd id) = 1 :=
+  gcd_div_eq_one s hx hnz
+#align finset.polynomial.gcd_div_id_eq_one Finset.Polynomial.gcd_div_id_eq_one
+
+end
+
+end Polynomial
+
+end Finset