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: tidy various files #3996

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: tidy various files #3996

wants to merge 1 commit into from

Conversation

Ruben-VandeVelde
Copy link
Collaborator

Open in Gitpod

@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-review The author would like community review of the PR label May 15, 2023
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot 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 15, 2023
@fpvandoorn
Copy link
Member

bors crashed, so I'm re-borsing

bors merge

bors bot pushed a commit that referenced this pull request May 15, 2023
@Ruben-VandeVelde
chore: tidy various files (#3996)
9ec7de3
@bors
Copy link

bors bot commented May 15, 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: tidy various files [Merged by Bors] - chore: tidy various files May 15, 2023
@bors bors bot closed this May 15, 2023
@bors bors bot deleted the various-tidy branch May 15, 2023 10:55
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
No reviews
Assignees
No one assigned
Labels
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
3 participants
@Ruben-VandeVelde @jcommelin @fpvandoorn