Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero#4766

Closed
eric-wieser wants to merge 11 commits intomasterfrom
pi-instances
Closed

[Merged by Bors] - feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero#4766
eric-wieser wants to merge 11 commits intomasterfrom
pi-instances

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Oct 24, 2020

@eric-wieser eric-wieser requested a review from urkud October 24, 2020 17:07
@eric-wieser eric-wieser changed the title Pi instances for nontrivial and monoid_with_zero feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero Oct 24, 2020
@urkud
Copy link
Copy Markdown
Member

urkud commented Oct 24, 2020

The proof of nontrivial shouldn't depend on [has_zero]. Instead, you should have

def pi.nontrivial' {α} {β : α → Sort*} [Π j, nonempty (β j)] (i : α) [nontrivial β i] : nontrivial (Π i, β i) := sorry

instance pi.nontrivial {α} [inhabited α] {β : α → Sort*} [Π i, nonempty (β i)] [nontrivial (deafult α)] : nontrivial (Π i, β i) :=
pi.nontrivial' (default α)

@eric-wieser
Copy link
Copy Markdown
Member Author

eric-wieser commented Oct 24, 2020

Good point, I've updated to use those dependencies instead.

eric-wieser
eric-wieser commented Oct 25, 2020
View reviewed changes
@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Oct 25, 2020
eric-wieser
eric-wieser commented Oct 25, 2020
View reviewed changes
Vierkantor
Vierkantor approved these changes Oct 27, 2020
View reviewed changes
@Vierkantor Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 27, 2020
eric-wieser
eric-wieser commented Oct 27, 2020
View reviewed changes
@eric-wieser @Vierkantor
Apply suggestions from code review
c620449 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Vierkantor
Vierkantor approved these changes Oct 27, 2020
View reviewed changes
Copy link
Copy Markdown
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. @urkud, any suggestions?

urkud
urkud reviewed Oct 28, 2020
View reviewed changes
@urkud
Copy link
Copy Markdown
Member

urkud commented Oct 28, 2020

Otherwise LGTM
bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 28, 2020

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser
eric-wieser commented Oct 30, 2020
View reviewed changes
@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR delegated The PR author may merge after reviewing final suggestions. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 30, 2020
@eric-wieser eric-wieser removed the awaiting-review The author would like community review of the PR label Oct 30, 2020
@eric-wieser
Copy link
Copy Markdown
Member Author

eric-wieser commented Oct 30, 2020

bors r+

bors bot pushed a commit that referenced this pull request Oct 30, 2020
@eric-wieser @urkud
feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (
c66ff49 
#4766)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link
Copy Markdown

bors bot commented Oct 30, 2020

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Oct 30, 2020
@eric-wieser @urkud
feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (
bfadf05 
#4766)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link
Copy Markdown

bors bot commented Oct 30, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero [Merged by Bors] - feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero Oct 30, 2020
@bors bors bot closed this Oct 30, 2020
@bors bors bot deleted the pi-instances branch October 30, 2020 17:07
lecopivo pushed a commit to lecopivo/mathlib that referenced this pull request Oct 31, 2020
@eric-wieser @urkud
feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (
6fac83f 
leanprover-community#4766)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
YaelDillies added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 20, 2024
@YaelDillies
chore: Move monoid with zero instances on pi types
820dfc5 
Move everything that could not be additivised out of `Algebra.Group.Pi.Lemmas`:
* `MulZeroClass`, `MulZeroOneClass`, etc... instances go to a new `Algebra.GroupWithZero.Pi` file. I credit Eric W. for leanprover-community/mathlib3#4766.
* `AddMonoidWithOne`, `AddGroupWithOne` instances go to `Algebra.Ring.Pi`.

Also fix a bunch of `single` that should have been `mulSingle`.
@YaelDillies YaelDillies mentioned this pull request Apr 20, 2024
Closed
YaelDillies added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 21, 2024
@YaelDillies
chore: Move monoid with zero instances on pi types
bc66dc9 
Move everything that can't be additivised out of `Algebra.Group.Pi.Lemmas`:
* `MulZeroClass`, `MulZeroOneClass`, etc... instances go to a new `Algebra.GroupWithZero.Pi` file. I credit Eric W. for leanprover-community/mathlib3#4766.
* `AddMonoidWithOne`, `AddGroupWithOne` instances go to `Algebra.Ring.Pi`.
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 29, 2024
@YaelDillies
chore: Move monoid with zero instances on pi types (#12286)
0a97fb7 
Move everything that can't be additivised out of `Algebra.Group.Pi.Lemmas`:
* `MulZeroClass`, `MulZeroOneClass`, etc... instances go to a new `Algebra.GroupWithZero.Pi` file. I credit Eric W. for leanprover-community/mathlib3#4766.
* `AddMonoidWithOne`, `AddGroupWithOne` instances go to `Algebra.Ring.Pi`.
apnelson1 pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2024
@YaelDillies @apnelson1
chore: Move monoid with zero instances on pi types (#12286)
e966319 
Move everything that can't be additivised out of `Algebra.Group.Pi.Lemmas`:
* `MulZeroClass`, `MulZeroOneClass`, etc... instances go to a new `Algebra.GroupWithZero.Pi` file. I credit Eric W. for leanprover-community/mathlib3#4766.
* `AddMonoidWithOne`, `AddGroupWithOne` instances go to `Algebra.Ring.Pi`.
callesonne pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 16, 2024
@YaelDillies @callesonne
chore: Move monoid with zero instances on pi types (#12286)
07deba7 
Move everything that can't be additivised out of `Algebra.Group.Pi.Lemmas`:
* `MulZeroClass`, `MulZeroOneClass`, etc... instances go to a new `Algebra.GroupWithZero.Pi` file. I credit Eric W. for leanprover-community/mathlib3#4766.
* `AddMonoidWithOne`, `AddGroupWithOne` instances go to `Algebra.Ring.Pi`.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

2 more reviewers

@urkud urkud urkud left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@eric-wieser @urkud @Vierkantor @bryangingechen