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 Geometry.Manifold.VectorBundle.SmoothSection #5736

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat: port Geometry.Manifold.VectorBundle.SmoothSection #5736

wants to merge 21 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jul 5, 2023 •
edited by github-actions bot

urkud and others added 21 commits July 5, 2023 08:54
@urkud
feat: port Data.Bundle
12aaeb1
@urkud
Initial file copy from mathport
ec7db3b
@urkud
automated fixes
0d18245 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@urkud
Snapshot
45bc797
@urkud
Update
94efb06
@urkud
Update SHA sums
a5e513e
@urkud
Long lines
763d411
@urkud
Fix a typo
eb22640
@urkud
Typo
ef65754
@urkud
Fix lint
1fa42b2
@urkud @negiizhao
Update Mathlib/Data/Bundle.lean
aa7096a 
Co-authored-by: negiizhao <egresf@gmail.com>
@urkud @negiizhao
Apply suggestions from code review
4be0fee 
Co-authored-by: negiizhao <egresf@gmail.com>
@urkud @negiizhao
Apply suggestions from code review
55399cf 
Co-authored-by: negiizhao <egresf@gmail.com>
@urkud @negiizhao
Apply suggestions from code review
3bc60ed 
Co-authored-by: negiizhao <egresf@gmail.com>
@urkud
Fix more comments
4bd6da1
@urkud
feat: port Geometry.Manifold.VectorBundle.SmoothSection
b5b7c60
@urkud
Initial file copy from mathport
ecfef8b
@urkud
automated fixes
d878288 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@urkud
Change import
d5337ca
@urkud
Fix compile
0f1030b
@urkud
auto: naming
a9d675a
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR which is still in the queue. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Jul 5, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

jcommelin
jcommelin approved these changes Jul 6, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin 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 merge

bors bot pushed a commit that referenced this pull request Jul 6, 2023
@urkud
feat: port Geometry.Manifold.VectorBundle.SmoothSection (#5736)
af1edf0
@semorrison semorrison added the ready-to-merge This PR has been sent to bors. label Jul 6, 2023
@bors
Copy link

bors bot commented Jul 6, 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 Geometry.Manifold.VectorBundle.SmoothSection [Merged by Bors] - feat: port Geometry.Manifold.VectorBundle.SmoothSection Jul 6, 2023
@bors bors bot closed this Jul 6, 2023
@bors bors bot deleted the port/Geometry.Manifold.VectorBundle.SmoothSection branch July 6, 2023 08:29
kbuzzard pushed a commit that referenced this pull request Jul 6, 2023
@urkud @kbuzzard
feat: port Geometry.Manifold.VectorBundle.SmoothSection (#5736)
e52e60e
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this pull request Jul 7, 2023
@urkud @qawbecrdtey
feat: port Geometry.Manifold.VectorBundle.SmoothSection (leanprover-c…
1edf59b 
…ommunity#5736)
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@urkud @semorrison
feat: port Geometry.Manifold.VectorBundle.SmoothSection (#5736)
8d57408
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

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
@urkud @semorrison @jcommelin