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(algebra, logic): Pi instances for nontrivial and monoid_with_zero #4766

Closed
wants to merge 11 commits into from
Closed

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

wants to merge 11 commits into from

Conversation

eric-wieser
Copy link
Member

@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
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
Member Author

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

@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Oct 25, 2020
Vierkantor
Vierkantor approved these changes Oct 27, 2020
View reviewed changes
src/logic/nontrivial.lean Outdated Show resolved Hide resolved
src/logic/nontrivial.lean Outdated Show resolved Hide resolved
src/logic/nontrivial.lean Outdated Show resolved Hide resolved
@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 @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
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
src/algebra/group/pi.lean Outdated Show resolved Hide resolved
@urkud
Copy link
Member

urkud commented Oct 28, 2020

Otherwise LGTM
bors d+

@bors
Copy link

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 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
Member Author

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

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

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/mathlib#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/mathlib#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/mathlib#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/mathlib#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/mathlib#4766.
* `AddMonoidWithOne`, `AddGroupWithOne` instances go to `Algebra.Ring.Pi`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

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.

None yet
4 participants
@eric-wieser @urkud @Vierkantor @bryangingechen