Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port Data.Polynomial.Module #3407

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat: port Data.Polynomial.Module #3407

wants to merge 28 commits into from

Conversation

linesthatinterlace
Copy link
Collaborator

@linesthatinterlace linesthatinterlace commented Apr 12, 2023 •
edited by Parcly-Taxel
Loading

Open in Gitpod

Parcly-Taxel and others added 14 commits April 11, 2023 13:40
@Parcly-Taxel @qawbecrdtey
@mattrobball @mcdoll
feat: port Analysis.NormedSpace.Basic (#3280)
f8e05e7 
For Tori & Hearth ♥
https://www.furaffinity.net/view/45973478
https://www.furaffinity.net/view/44859543



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
@Ruben-VandeVelde @Komyyy
feat: port Computability.Encoding (#2799)
1eaede3 
Co-authored-by: Komyyy <pol_tta@outlook.jp>
@EmilieUthaiwat
feat: port RingTheory.Polynomial.Eisenstein.Basic (#3382)
2d97a15
@eric-wieser @kim-em @Parcly-Taxel
feat: @[eqns] attribute to override equation lemmas (#3024)
0c711c2 
This is to help with #2960 and work around leanprover/lean4#2042.

Ideally we would inspect the function to find that it was declared as `| i, j => A j i` and generate `transpose_apply`, but that's not something I know how to do.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@YaelDillies @Parcly-Taxel
feat: Dot notation aliases (#3303)
613e4e7 
Match leanprover-community/mathlib3#18698 and a bit of leanprover-community/mathlib3#18785.

* [`algebra.divisibility.basic`@`70d50ecfd4900dd6d328da39ab7ebd516abe4025`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/divisibility/basic?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.euclidean_domain.basic`@`655994e298904d7e5bbd1e18c95defd7b543eb94`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/euclidean_domain/basic?range=655994e298904d7e5bbd1e18c95defd7b543eb94..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group.units`@`369525b73f229ccd76a6ec0e0e0bf2be57599768`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/units?range=369525b73f229ccd76a6ec0e0e0bf2be57599768..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.units.basic`@`70d50ecfd4900dd6d328da39ab7ebd516abe4025`..`df5e9937a06fdd349fc60106f54b84d47b1434f0`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/units/basic?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..df5e9937a06fdd349fc60106f54b84d47b1434f0)
* [`algebra.order.monoid.canonical.defs`@`de87d5053a9fe5cbde723172c0fb7e27e7436473`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/canonical/defs?range=de87d5053a9fe5cbde723172c0fb7e27e7436473..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.dvd.basic`@`e1bccd6e40ae78370f01659715d3c948716e3b7e`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/dvd/basic?range=e1bccd6e40ae78370f01659715d3c948716e3b7e..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.dvd.pow`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/dvd/pow?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.order.basic`@`728baa2f54e6062c5879a3e397ac6bac323e506f`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/order/basic?range=728baa2f54e6062c5879a3e397ac6bac323e506f..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.gcd.basic`@`a47cda9662ff3925c6df271090b5808adbca5b46`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/gcd/basic?range=a47cda9662ff3925c6df271090b5808adbca5b46..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.order.basic`@`26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/basic?range=26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`group_theory.perm.cycle.basic`@`92ca63f0fb391a9ca5f22d2409a6080e786d99f7`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/perm/cycle/basic?range=92ca63f0fb391a9ca5f22d2409a6080e786d99f7..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.divisors`@`f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/divisors?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.pythagorean_triples`@`70fd9563a21e7b963887c9360bd29b2393e6225a`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/pythagorean_triples?range=70fd9563a21e7b963887c9360bd29b2393e6225a..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.zsqrtd.basic`@`7ec294687917cbc5c73620b4414ae9b5dd9ae1b4`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/zsqrtd/basic?range=7ec294687917cbc5c73620b4414ae9b5dd9ae1b4..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`ring_theory.multiplicity`@`ceb887ddf3344dab425292e497fa2af91498437c`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/multiplicity?range=ceb887ddf3344dab425292e497fa2af91498437c..e8638a0fcaf73e4500469f368ef9494e495099b3)



Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@Parcly-Taxel
chore: forward port mathlib#17611, 18742, 18198, 18520 (#3389)
13413a3 
SHA-only updates:
* leanprover-community/mathlib3#17611 – `CategoryTheory.Sites.Sheaf` already uses `aesop_cat` at this location, nothing to port.
* leanprover-community/mathlib3#18742 – fiber spelling, which is all of the changes to `Topology.FiberBundle.Trivialization`, is already in mathlib4.
* leanprover-community/mathlib3#18198 – `FunLike` change to `Data.PEquiv` is already in mathlib4.

Substantative forward port:
* leanprover-community/mathlib3#18520



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
@j-loreaux
feat: port Analysis.Normed.Order.Basic (#3391)
fd26b03
@gebner
feat: irreducible_def: support protected, equation lemmas (#3395)
e93a493
@j-loreaux
feat: port Analysis.NormedSpace.RieszLemma (#3397)
1a72af4
@vihdzp
feat: port #15071 (#3248)
f5de05f 
* [`order.basic`@`de87d5053a9fe5cbde723172c0fb7e27e7436473`..`210657c4ea4a4a7b234392f70a3a2a83346dfa90`](https://leanprover-community.github.io/mathlib-port-status/file/order/basic?range=de87d5053a9fe5cbde723172c0fb7e27e7436473..210657c4ea4a4a7b234392f70a3a2a83346dfa90)
* [`order.well_founded`@`1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e`..`210657c4ea4a4a7b234392f70a3a2a83346dfa90`](https://leanprover-community.github.io/mathlib-port-status/file/order/well_founded?range=1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e..210657c4ea4a4a7b234392f70a3a2a83346dfa90)
* [`order.order_iso_nat`@`6623e6af705e97002a9054c1c05a980180276fc1`..`210657c4ea4a4a7b234392f70a3a2a83346dfa90`](https://leanprover-community.github.io/mathlib-port-status/file/order/order_iso_nat?range=6623e6af705e97002a9054c1c05a980180276fc1..210657c4ea4a4a7b234392f70a3a2a83346dfa90)
* [`order.compactly_generated`@`861a26926586cd46ff80264d121cdb6fa0e35cc1`..`210657c4ea4a4a7b234392f70a3a2a83346dfa90`](https://leanprover-community.github.io/mathlib-port-status/file/order/compactly_generated?range=861a26926586cd46ff80264d121cdb6fa0e35cc1..210657c4ea4a4a7b234392f70a3a2a83346dfa90)
* [`ring_theory.noetherian`@`da420a8c6dd5bdfb85c4ced85c34388f633bc6ff`..`210657c4ea4a4a7b234392f70a3a2a83346dfa90`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/noetherian?range=da420a8c6dd5bdfb85c4ced85c34388f633bc6ff..210657c4ea4a4a7b234392f70a3a2a83346dfa90)

Mathlib 3: leanprover-community/mathlib3#15071
@YaelDillies
feat: Induction principle for powers (#3278)
56304e9 
leanprover-community/mathlib3#18668

* [`algebra.group_power.lemmas`@`05101c3df9d9cfe9430edc205860c79b6d660102`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_power/lemmas?range=05101c3df9d9cfe9430edc205860c79b6d660102..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`group_theory.submonoid.membership`@`2ec920d35348cb2d13ac0e1a2ad9df0fdf1a76b4`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/submonoid/membership?range=2ec920d35348cb2d13ac0e1a2ad9df0fdf1a76b4..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`group_theory.subgroup.zpowers`@`f93c11933efbc3c2f0299e47b8ff83e9b539cbf6`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/subgroup/zpowers?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`group_theory.subgroup.pointwise`@`c10e724be91096453ee3db13862b9fb9a992fef2`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/subgroup/pointwise?range=c10e724be91096453ee3db13862b9fb9a992fef2..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`ring_theory.int.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/int/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..e655e4ea5c6d02854696f97494997ba4c31be802)
@linesthatinterlace
feat: port Data.Polynomial.Module
9aa9dc3
@linesthatinterlace
Initial file copy from mathport
0d0a9f4
@linesthatinterlace
automated fixes
3cd3673 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@linesthatinterlace linesthatinterlace added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 12, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 12, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 13, 2023
@linesthatinterlace linesthatinterlace added help-wanted The author needs attention to resolve issues and removed WIP Work in progress labels Apr 13, 2023
@linesthatinterlace
Copy link
Collaborator Author

I've done as much as I can easily fix here, but I'm having issues with the definition of comp that I can't get past. Would appreciate some help.

@linesthatinterlace linesthatinterlace added awaiting-review and removed help-wanted The author needs attention to resolve issues labels Apr 17, 2023
@linesthatinterlace
Copy link
Collaborator Author

Thanks for the comp definition @int-y1. I have fixed the remaining proofs, fixed documentation and checked lints, and this now requires review.

@kim-em
Copy link
Contributor

kim-em commented Apr 17, 2023

bors d+

@bors
Copy link

bors bot commented Apr 17, 2023

✌️ linesthatinterlace can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@linesthatinterlace
Copy link
Collaborator Author

bors r+

@bors
Copy link

bors bot commented Apr 20, 2023

Canceled.

@linesthatinterlace
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 21, 2023
@Parcly-Taxel @Ruben-VandeVelde
@EmilieUthaiwat @eric-wieser @YaelDillies @j-loreaux @gebner @vihdzp @linesthatinterlace @int-y1 @kim-em
feat: port Data.Polynomial.Module (#3407)
a1e24be 


Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: EmilieUthaiwat <emiliepathum@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Wrenna Robson <wren.robson@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
@bors
Copy link

bors bot commented Apr 21, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Polynomial.Module [Merged by Bors] - feat: port Data.Polynomial.Module Apr 21, 2023
@bors bors bot closed this Apr 21, 2023
@bors bors bot deleted the port/Data.Polynomial.Module branch April 21, 2023 15:26
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
@Parcly-Taxel @Ruben-VandeVelde
@EmilieUthaiwat @eric-wieser @YaelDillies @j-loreaux @gebner @vihdzp @linesthatinterlace @int-y1 @kim-em @kbuzzard
feat: port Data.Polynomial.Module (#3407)
3b5a68a 


Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: EmilieUthaiwat <emiliepathum@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Wrenna Robson <wren.robson@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
kim-em added a commit that referenced this pull request May 10, 2023
@Parcly-Taxel @Ruben-VandeVelde
@EmilieUthaiwat @eric-wieser @YaelDillies @j-loreaux @gebner @vihdzp @linesthatinterlace @int-y1 @kim-em
feat: port Data.Polynomial.Module (#3407)
ba4db64 


Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: EmilieUthaiwat <emiliepathum@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Wrenna Robson <wren.robson@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
@Parcly-Taxel @Ruben-VandeVelde
@EmilieUthaiwat @eric-wieser @YaelDillies @j-loreaux @gebner @vihdzp @linesthatinterlace @int-y1 @kim-em @hrmacbeth
feat: port Data.Polynomial.Module (#3407)
39969d5 


Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: EmilieUthaiwat <emiliepathum@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Wrenna Robson <wren.robson@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
@Parcly-Taxel @Ruben-VandeVelde
@EmilieUthaiwat @eric-wieser @YaelDillies @j-loreaux @gebner @vihdzp @linesthatinterlace @int-y1 @kim-em @hrmacbeth
feat: port Data.Polynomial.Module (#3407)
73eac67 


Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: EmilieUthaiwat <emiliepathum@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Wrenna Robson <wren.robson@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.