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] - chore: forward port leanprover-community/mathlib#18946 #3888

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - chore: forward port leanprover-community/mathlib#18946 #3888

wants to merge 5 commits into from

Conversation

collares
Copy link
Collaborator

@collares collares commented May 10, 2023 •
edited

@collares collares added awaiting-review The author would like community review of the PR mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels May 10, 2023
@eric-wieser eric-wieser mentioned this pull request May 13, 2023
Closed
1 task
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 14, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 14, 2023
eric-wieser
eric-wieser approved these changes May 14, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors merge

Thanks!

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 14, 2023
bors bot pushed a commit that referenced this pull request May 14, 2023
@collares @eric-wieser
chore: forward port leanprover-community/mathlib#18946 (#3888)
e066c3b 
Forward port leanprover-community/mathlib#18946.


Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented May 14, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: forward port leanprover-community/mathlib#18946 [Merged by Bors] - chore: forward port leanprover-community/mathlib#18946 May 14, 2023
@bors bors bot closed this May 14, 2023
@bors bors bot deleted the collares/ennreal-fwport branch May 14, 2023 22:25
pechersky added a commit that referenced this pull request May 15, 2023
@pechersky
Squashed commit of the following:
e8ce255 
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@collares @eric-wieser @YaelDillies @semorrison