Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Algebra.GCDMonoid.Div (#3143)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
- Loading branch information
1 parent
7fb2ff3
commit f8741cb
Showing
2 changed files
with
102 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |