Skip to content

[Merged by Bors] - feat: port Algebra.Star.Free#3007

Closed
Parcly-Taxel wants to merge 15 commits intomasterfrom
port/Algebra.Star.Free
Closed

[Merged by Bors] - feat: port Algebra.Star.Free#3007
Parcly-Taxel wants to merge 15 commits intomasterfrom
port/Algebra.Star.Free

Conversation

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

@Parcly-Taxel Parcly-Taxel commented Mar 21, 2023 •
edited
Loading

@Parcly-Taxel
feat: port Algebra.Star.Free
9961b16
@Parcly-Taxel
Initial file copy from mathport
698e047
@Parcly-Taxel
automated fixes
33f661e 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Parcly-Taxel
Fix errors (but noncomputable?)
a065502
@Parcly-Taxel Parcly-Taxel added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Mar 21, 2023
eric-wieser
eric-wieser reviewed Mar 21, 2023
View reviewed changes
@Parcly-Taxel Parcly-Taxel mentioned this pull request Mar 21, 2023
Closed
@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Mar 23, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Mar 23, 2023

This PR/issue depends on:

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Mar 23, 2023

Can you merge master to make the diff shrink?

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator Author

Parcly-Taxel commented Mar 23, 2023

Can you merge master to make the diff shrink?

Done.

eric-wieser
eric-wieser reviewed Mar 23, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 23, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 23, 2023
View reviewed changes
Parcly-Taxel and others added 2 commits March 24, 2023 00:30
@Parcly-Taxel @eric-wieser
Update Mathlib/Algebra/Star/Free.lean
9d5ebac 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@Parcly-Taxel @eric-wieser
The same
dcea19a 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Mar 24, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 24, 2023
bors bot pushed a commit that referenced this pull request Mar 24, 2023
@Parcly-Taxel @eric-wieser
feat: port Algebra.Star.Free (#3007)
44e938c 
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Mar 24, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Star.Free [Merged by Bors] - feat: port Algebra.Star.Free Mar 24, 2023
@bors bors bot closed this Mar 24, 2023
@bors bors bot deleted the port/Algebra.Star.Free branch March 24, 2023 13:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser 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.

4 participants

@Parcly-Taxel @kim-em @eric-wieser @ChrisHughes24