[Merged by Bors] - feat(data/finset/pointwise): |s| ∣ |s * t| #5385
Conversation
urkud
added
awaiting-review
| distinct!), then the size of `t` divides the size of `s + t`."] | ||
| theorem card_dvd_card_mul_right {s t : Finset α} : | ||
| ((· • t) '' (s : Set α)).PairwiseDisjoint id → t.card ∣ (s * t).card := | ||
| card_dvd_card_image₂_right fun _ _ => mul_right_injective _ |
There was a problem hiding this comment.
| card_dvd_card_image₂_right fun _ _ => mul_right_injective _ | |
| card_dvd_card_smul_right |
I think this is why I didn't make it a lemma.
There was a problem hiding this comment.
It's already on the queue... I see that these two lemmas are defeq but we don't drop mul_assoc because we have smul_assoc etc.
There was a problem hiding this comment.
Arf, we really need maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
1 similar comment
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
bors merge |
github-actions
bot
added
ready-to-merge
Forward-port leanprover-community/mathlib#18663 Also add a missing lemma.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Forward-port leanprover-community/mathlib#18663 Also add a missing lemma.
Forward-port leanprover-community/mathlib#18663 Also add a missing lemma.
Forward-port leanprover-community/mathlib#18663 Also add a missing lemma.
Forward-port leanprover-community/mathlib#18663 Also add a missing lemma.
Forward-port leanprover-community/mathlib#18663 Also add a missing lemma.
Forward-port leanprover-community/mathlib#18663
Also add a missing lemma.
@YaelDillies In the added lemma, what is the canonical way to write the assumption? Use
smul(as I did) or someFinset.image?