Skip to content

[Merged by Bors] - feat: Port algebra.punit_instances#1319

Closed
arienmalec wants to merge 45 commits intomasterfrom
port/Algebra.PUnitInstances
Closed

[Merged by Bors] - feat: Port algebra.punit_instances#1319
arienmalec wants to merge 45 commits intomasterfrom
port/Algebra.PUnitInstances

Conversation

@arienmalec
Copy link
Copy Markdown
Contributor

@arienmalec arienmalec commented Jan 3, 2023 •
edited by jcommelin
Loading

@arienmalec arienmalec added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jan 3, 2023
@fpvandoorn fpvandoorn mentioned this pull request Jan 4, 2023
Closed
@arienmalec arienmalec added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review and removed WIP Work in progress labels Jan 4, 2023
@hrmacbeth hrmacbeth added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 5, 2023
@arienmalec arienmalec added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 5, 2023
@arienmalec
Copy link
Copy Markdown
Contributor Author

arienmalec commented Jan 5, 2023

Who knew a file that's all trival defs and lemmas could be so difficult.

arienmalec and others added 2 commits January 5, 2023 11:56
@arienmalec
star -> unit throughout
1a31546
@arienmalec @hrmacbeth
Update Mathlib/Algebra/PUnitInstances.lean
8930718 
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
bors bot pushed a commit that referenced this pull request Jan 6, 2023
@fpvandoorn
fix: add PUnit/PEmpty to additive dict (#1330)
8dd499b 
This should fix the problems in [#1319](#1319)
@kim-em kim-em added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is 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 Jan 6, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jan 9, 2023

This PR/issue depends on:

@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 Jan 9, 2023
@hrmacbeth
Copy link
Copy Markdown
Member

hrmacbeth commented Jan 9, 2023

Thanks!

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 9, 2023
bors bot pushed a commit that referenced this pull request Jan 9, 2023
@fpvandoorn @arienmalec @hrmacbeth
feat: Port algebra.punit_instances (#1319)
39a53f6 
Port of algebra.punit_instances

- [x] depends on: #1330
- [x] depends on: #1314

Co-authored-by: Arien Malec <arien.malec@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
@bors
Copy link
Copy Markdown

bors bot commented Jan 9, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: Port algebra.punit_instances [Merged by Bors] - feat: Port algebra.punit_instances Jan 9, 2023
@bors bors bot closed this Jan 9, 2023
@bors bors bot deleted the port/Algebra.PUnitInstances branch January 9, 2023 20:45
Ruben-VandeVelde pushed a commit that referenced this pull request Jan 9, 2023
@fpvandoorn @arienmalec
@hrmacbeth @Ruben-VandeVelde
feat: Port algebra.punit_instances (#1319)
fc69f44 
Port of algebra.punit_instances

- [x] depends on: #1330
- [x] depends on: #1314

Co-authored-by: Arien Malec <arien.malec@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
jcommelin pushed a commit that referenced this pull request Jan 23, 2023
@fpvandoorn @arienmalec
@hrmacbeth @jcommelin
feat: Port algebra.punit_instances (#1319)
65fc2e7 
Port of algebra.punit_instances

- [x] depends on: #1330
- [x] depends on: #1314

Co-authored-by: Arien Malec <arien.malec@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hrmacbeth hrmacbeth hrmacbeth 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

@arienmalec @hrmacbeth @kim-em @fpvandoorn