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.
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
feat(*): some simple lemmas about sets and finite sets #1903
Conversation
Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
This reverts commit 17c89a8. It breaks compile if we rewrite right to left.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is good for me. @ChrisHughes24 , if you are happy, you get set this to ready to merge.
exact fin.cases (or.inl rfl) (λ i, or.inr ⟨i, trivial, rfl⟩) m | ||
end | ||
|
||
theorem fin.prod_univ_succ [comm_monoid β] {n:ℕ} (f : fin n.succ → β) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe add a comment why this does not work with to_additive
(I guess this is because of the 0
?) and that the to_additive
version will be registered in fin.sum_univ_succ
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As far as I understand, it's because +1
is used somewhere in the proof, and to_additive
tries to replace it with +0
.
…mmunity#1903) * feat(*): some simple lemmas about sets and finite sets * More lemmas, simplify proofs * Introduce `finsup.nonempty` and use it. * Update src/algebra/big_operators.lean Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> * Revert "Update src/algebra/big_operators.lean" This reverts commit 17c89a8. It breaks compile if we rewrite right to left. * simp, to_additive * Add a missing docstring Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…mmunity#1903) * feat(*): some simple lemmas about sets and finite sets * More lemmas, simplify proofs * Introduce `finsup.nonempty` and use it. * Update src/algebra/big_operators.lean Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> * Revert "Update src/algebra/big_operators.lean" This reverts commit 17c89a8. It breaks compile if we rewrite right to left. * simp, to_additive * Add a missing docstring Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list