Skip to content

[Merged by Bors] - feat: port Analysis.Complex.Basic#3930

Closed
urkud wants to merge 11 commits intomasterfrom
port/Analysis.Complex.Basic
Closed

[Merged by Bors] - feat: port Analysis.Complex.Basic#3930
urkud wants to merge 11 commits intomasterfrom
port/Analysis.Complex.Basic

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented May 12, 2023

Open in Gitpod

urkud added 5 commits May 13, 2023 15:24
@urkud
feat: port Analysis.Complex.Basic
5a77952
@urkud
Initial file copy from mathport
e9cd350
@urkud
automated fixes
80813ca 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@urkud
Fix here and there
085e484
@urkud
Fix more
439cf12
@urkud urkud force-pushed the port/Analysis.Complex.Basic branch from 060764e to 439cf12 Compare May 13, 2023 20:24
@pechersky pechersky mentioned this pull request May 14, 2023
Closed
1 task
@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 May 15, 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 May 15, 2023
@urkud urkud added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels May 15, 2023
dupuisf
dupuisf reviewed May 15, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@dupuisf dupuisf left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

@bors
Copy link
Copy Markdown

bors bot commented May 15, 2023

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

@kim-em kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels May 15, 2023
@urkud @dupuisf
Update Mathlib/Analysis/Complex/Basic.lean
ae973bf 
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
@urkud
Copy link
Copy Markdown
Member Author

urkud commented May 15, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label May 15, 2023
bors bot pushed a commit that referenced this pull request May 15, 2023
@urkud @pechersky @Parcly-Taxel
feat: port Analysis.Complex.Basic (#3930)
0c89172 
Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
@bors
Copy link
Copy Markdown

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 feat: port Analysis.Complex.Basic [Merged by Bors] - feat: port Analysis.Complex.Basic May 15, 2023
@bors bors bot closed this May 15, 2023
@bors bors bot deleted the port/Analysis.Complex.Basic branch May 15, 2023 21:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dupuisf dupuisf dupuisf left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib-port This is a port of a theory file from mathlib. 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.

5 participants

@urkud @dupuisf @kim-em @pechersky @Parcly-Taxel