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
[Merged by Bors] - feat: demote the instance Fintype.ofIsEmpty to a def #8816
Conversation
Mathlib/Data/Fintype/Card.lean
Outdated
/-- Note: this lemma is specifically about `Fintype.of_is_empty`. For a statement about | ||
arbitrary `Fintype` instances, use `Fintype.card_eq_zero_iff`. -/ | ||
@[simp] | ||
theorem card_of_isEmpty [IsEmpty α] : Fintype.card α = 0 := | ||
rfl | ||
#align fintype.card_of_is_empty Fintype.card_of_isEmpty |
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.
We should keep this lemma, but stated using a letI := Fintype.ofIsEmpty
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.
It is a particular case of card_eq_zero
, so why keep it?
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.
Because this one works with dsimp
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.
ok, I've added it back.
Thanks! 🎉 |
Rationale: this instance creates (empty) data out of nothing, which may conflict with other data. If you have in the context `[Fintype i]` and case on whether `i` is empty or not, then this gave two non-defeq instances of `[Fintype i]` around.
Build failed: |
Please merge |
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Rationale: this instance creates (empty) data out of nothing, which may conflict with other data. If you have in the context `[Fintype i]` and case on whether `i` is empty or not, then this gave two non-defeq instances of `[Fintype i]` around.
Pull request successfully merged into master. Build succeeded: |
Rationale: this instance creates (empty) data out of nothing, which may conflict with other data. If you have in the context `[Fintype i]` and case on whether `i` is empty or not, then this gave two non-defeq instances of `[Fintype i]` around.
Rationale: this instance creates (empty) data out of nothing, which may conflict with other data. If you have in the context
[Fintype i]
and case on whetheri
is empty or not, then this gave two non-defeq instances of[Fintype i]
around.