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 Algebra.Module.Submodule.Basic #1888

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat: port Algebra.Module.Submodule.Basic #1888

wants to merge 11 commits into from

Conversation

Ruben-VandeVelde
Copy link
Collaborator

Open in Gitpod

@Ruben-VandeVelde
Initial file copy from mathport
c6dc835
@Ruben-VandeVelde
automated fixes
4633b03 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@Ruben-VandeVelde Ruben-VandeVelde added help-wanted The author needs attention to resolve issues mathlib-port This is a port of a theory file from mathlib. labels Jan 27, 2023
@jcommelin
Copy link
Member

Please rebase on master.

@Ruben-VandeVelde Ruben-VandeVelde force-pushed the port/Algebra.Module.Submodule.Basic branch from ff91d23 to 536dddc Compare January 27, 2023 16:08
@Vierkantor
Copy link
Contributor

I'm going in 10 to 15 minutes. Everything should build and lint correctly, we need to run the other fixing scripts and check the names and docstrings.

@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 27, 2023
bors bot pushed a commit that referenced this pull request Jan 27, 2023
@Ruben-VandeVelde @Vierkantor @jcommelin
feat: port Algebra.Module.Submodule.Basic (#1888)
2ee6978 
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
@jcommelin jcommelin removed the help-wanted The author needs attention to resolve issues label Jan 27, 2023
@bors
Copy link

bors bot commented Jan 27, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Module.Submodule.Basic [Merged by Bors] - feat: port Algebra.Module.Submodule.Basic Jan 27, 2023
@bors bors bot closed this Jan 27, 2023
@bors bors bot deleted the port/Algebra.Module.Submodule.Basic branch January 27, 2023 18:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
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.

None yet
3 participants
@Ruben-VandeVelde @jcommelin @Vierkantor