Skip to content

[Merged by Bors] - fix: add PUnit/PEmpty to additive dict#1330

Closed
fpvandoorn wants to merge 1 commit intomasterfrom
toAdditivePUnit
Closed

[Merged by Bors] - fix: add PUnit/PEmpty to additive dict#1330
fpvandoorn wants to merge 1 commit intomasterfrom
toAdditivePUnit

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Jan 4, 2023

This should fix the problems in #1319

@fpvandoorn fpvandoorn added awaiting-review t-meta Tactics, attributes or user commands labels Jan 4, 2023
@arienmalec arienmalec mentioned this pull request Jan 4, 2023
Closed
2 tasks
@gebner
Copy link
Copy Markdown
Member

gebner commented Jan 6, 2023

We have the same attributes in mathlib3.

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 6, 2023
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)
@bors
Copy link
Copy Markdown

bors bot commented Jan 6, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix: add PUnit/PEmpty to additive dict [Merged by Bors] - fix: add PUnit/PEmpty to additive dict Jan 6, 2023
@bors bors bot closed this Jan 6, 2023
@bors bors bot deleted the toAdditivePUnit branch January 6, 2023 02:05
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>
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

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@fpvandoorn @gebner