-
Notifications
You must be signed in to change notification settings - Fork 259
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.
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
[Merged by Bors] - chore(*): forward-port #18947 #3925
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors merge
Thanks!
* [`ring_theory.ideal.quotient`@`2f39bcbc98f8255490f8d4562762c9467694c809`..`949dc57e616a621462062668c9f39e4e17b64b69`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/ideal/quotient?range=2f39bcbc98f8255490f8d4562762c9467694c809..949dc57e616a621462062668c9f39e4e17b64b69) * [`data.polynomial.basic`@`2651125b48fc5c170ab1111afd0817c903b1fc6c`..`949dc57e616a621462062668c9f39e4e17b64b69`](https://leanprover-community.github.io/mathlib-port-status/file/data/polynomial/basic?range=2651125b48fc5c170ab1111afd0817c903b1fc6c..949dc57e616a621462062668c9f39e4e17b64b69) * [`algebra.monoid_algebra.basic`@`f69db8cecc668e2d5894d7e9bfc491da60db3b9f`..`949dc57e616a621462062668c9f39e4e17b64b69`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/monoid_algebra/basic?range=f69db8cecc668e2d5894d7e9bfc491da60db3b9f..949dc57e616a621462062668c9f39e4e17b64b69)
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
commit 2dd59f7 Author: Parcly Taxel <reddeloostw@gmail.com> Date: Mon May 15 19:40:51 2023 +0800 Fix names commit 82e93da Author: Parcly Taxel <reddeloostw@gmail.com> Date: Mon May 15 19:34:40 2023 +0800 lint commit 02c1971 Merge: be76323 9ec7de3 Author: Parcly Taxel <reddeloostw@gmail.com> Date: Mon May 15 19:29:49 2023 +0800 Merge branch 'master' into port/Analysis.Complex.Basic commit 9ec7de3 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Mon May 15 10:07:02 2023 +0000 chore: tidy various files (#3996) commit 9bf37f6 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Mon May 15 10:07:00 2023 +0000 feat: port CategoryTheory.Sites.InducedTopology (#3995) Co-authored-by: Moritz Firsching <firsching@google.com> commit 89672a9 Author: Chris Hughes <chrishughes24@gmail.com> Date: Mon May 15 10:06:59 2023 +0000 chore Order/Chain: unused arguments (#3986) commit ae53970 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Mon May 15 10:06:58 2023 +0000 feat: port CategoryTheory.CofilteredSystem (#3977) commit 23a970b Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Mon May 15 10:06:56 2023 +0000 feat: port Order.Category.FrmCat (#3970) commit a2ab29c Author: Pol_tta <pol_tta@outlook.jp> Date: Mon May 15 10:06:55 2023 +0000 doc: fix the docs on `ModelTheory/*` (#3968) commit 618546f Author: Moritz Doll <moritz.doll@googlemail.com> Date: Mon May 15 10:06:54 2023 +0000 feat: port Analysis.Calculus.TangentCone (#3636) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> commit 0de17db Author: Pol_tta <pol_tta@outlook.jp> Date: Mon May 15 09:49:01 2023 +0000 refactor: rename `FirstOrder.Language.Theory.CompleteTheory.subset` to `FirstOrder.Language.Theory.completeTheory.subset` (#3990) commit c442325 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Mon May 15 09:05:58 2023 +0000 feat: port Data.Polynomial.Laurent (#2953) Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> commit 31f0309 Author: Kevin Buzzard <k.buzzard@imperial.ac.uk> Date: Mon May 15 06:06:55 2023 +0000 feat: port CategoryTheory.Sites.DenseSubsite (#3985) Mostly straightforward. Had to fight with `simp` once and the typeclass inference system a couple of times. commit 4bc088b Author: Scott Morrison <scott@tqft.net> Date: Mon May 15 05:38:52 2023 +0000 chore: update zulip bot for maintainer merge (#3992) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit ffd0ad4 Author: Eric Rodriguez <ericrboidi@gmail.com> Date: Sun May 14 22:49:41 2023 +0000 chore(*): forward-port #18947 (#3925) * [`ring_theory.ideal.quotient`@`2f39bcbc98f8255490f8d4562762c9467694c809`..`949dc57e616a621462062668c9f39e4e17b64b69`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/ideal/quotient?range=2f39bcbc98f8255490f8d4562762c9467694c809..949dc57e616a621462062668c9f39e4e17b64b69) * [`data.polynomial.basic`@`2651125b48fc5c170ab1111afd0817c903b1fc6c`..`949dc57e616a621462062668c9f39e4e17b64b69`](https://leanprover-community.github.io/mathlib-port-status/file/data/polynomial/basic?range=2651125b48fc5c170ab1111afd0817c903b1fc6c..949dc57e616a621462062668c9f39e4e17b64b69) * [`algebra.monoid_algebra.basic`@`f69db8cecc668e2d5894d7e9bfc491da60db3b9f`..`949dc57e616a621462062668c9f39e4e17b64b69`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/monoid_algebra/basic?range=f69db8cecc668e2d5894d7e9bfc491da60db3b9f..949dc57e616a621462062668c9f39e4e17b64b69) commit e066c3b Author: Mauricio Collares <mauricio@collares.org> Date: Sun May 14 21:50:26 2023 +0000 chore: forward port leanprover-community/mathlib#18946 (#3888) Forward port leanprover-community/mathlib#18946. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit be76323 Author: Yakov Pechersky <ypechersky@treeline.bio> Date: Sun May 14 16:38:53 2023 -0400 linting commit c03b4d2 Author: Yakov Pechersky <ypechersky@treeline.bio> Date: Sun May 14 15:46:38 2023 -0400 Fix errors commit 439cf12 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Sat May 13 01:48:01 2023 -0500 Fix more commit 085e484 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Fri May 12 07:55:26 2023 -0500 Fix here and there commit 80813ca Author: Yury G. Kudryashov <urkud@urkud.name> Date: Thu May 11 20:42:55 2023 -0500 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit e9cd350 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Thu May 11 20:42:55 2023 -0500 Initial file copy from mathport commit 5a77952 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Thu May 11 20:42:55 2023 -0500 feat: port Analysis.Complex.Basic
ring_theory.ideal.quotient
@2f39bcbc98f8255490f8d4562762c9467694c809
..949dc57e616a621462062668c9f39e4e17b64b69
data.polynomial.basic
@2651125b48fc5c170ab1111afd0817c903b1fc6c
..949dc57e616a621462062668c9f39e4e17b64b69
algebra.monoid_algebra.basic
@f69db8cecc668e2d5894d7e9bfc491da60db3b9f
..949dc57e616a621462062668c9f39e4e17b64b69