[Merged by Bors] - chore(data/fin,data/finset): a few lemmas #7168
Conversation
| by simpa using fintype.sum_pow_mul_eq_add_pow (fin n) a b | ||
|
|
||
| lemma fin.prod_const [comm_monoid α] (n : ℕ) (x : α) : ∏ i : fin n, x = x ^ n := by simp |
There was a problem hiding this comment.
This should be @[to_additive] right?
There was a problem hiding this comment.
to_additive can't deal with pow by itself, so we'll need a manual sum_const lemma.
There was a problem hiding this comment.
We still should connect these two lemmas with @[to_additive] after proving them both, right?
There was a problem hiding this comment.
No, to_additive won't be able to use this because it'll fail to match the types of RHS.
| @@ -961,6 +964,14 @@ instance finset.fintype [fintype α] : fintype (finset α) := | |||
| fintype.card (finset α) = 2 ^ (fintype.card α) := | |||
| finset.card_powerset finset.univ | |||
|
|
|||
| @[simp] lemma fintype.card_finset_len [fintype α] (k : ℕ) : | |||
| fintype.card {s : finset α // s.card = k} = nat.choose (fintype.card α) k := | |||
There was a problem hiding this comment.
Is the LHS the canonical way to talk about the number of elements satisfying a property? I would expect it to be (finset.univ.filter ...).card
| by simpa using fintype.sum_pow_mul_eq_add_pow (fin n) a b | ||
|
|
||
| lemma fin.prod_const [comm_monoid α] (n : ℕ) (x : α) : ∏ i : fin n, x = x ^ n := by simp |
There was a problem hiding this comment.
We still should connect these two lemmas with @[to_additive] after proving them both, right?
|
Note: I unresolved an earlier comment. LGTM (independent of how you deal with my comment on bors d+ |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
fpvandoorn
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
* `fin.heq_fun_iff`: use `Sort*` instead of `Type*`; * `fin.cast_refl`: take `h : n = n := rfl` as an argument; * `fin.cast_to_equiv`, `fin.cast_eq_cast`: relate `fin.cast` to `_root_.cast`; * `finset.map_cast_heq`: new lemma; * `finset.subset_univ`: add `@[simp]`; * `card_finset_fin_le`, `fintype.card_finset_len`, `fin.prod_const` : new lemmas; * `order_iso.refl`: new definition.
|
Build failed (retrying...): |
* `fin.heq_fun_iff`: use `Sort*` instead of `Type*`; * `fin.cast_refl`: take `h : n = n := rfl` as an argument; * `fin.cast_to_equiv`, `fin.cast_eq_cast`: relate `fin.cast` to `_root_.cast`; * `finset.map_cast_heq`: new lemma; * `finset.subset_univ`: add `@[simp]`; * `card_finset_fin_le`, `fintype.card_finset_len`, `fin.prod_const` : new lemmas; * `order_iso.refl`: new definition.
|
Canceled. |
|
bors merge |
* `fin.heq_fun_iff`: use `Sort*` instead of `Type*`; * `fin.cast_refl`: take `h : n = n := rfl` as an argument; * `fin.cast_to_equiv`, `fin.cast_eq_cast`: relate `fin.cast` to `_root_.cast`; * `finset.map_cast_heq`: new lemma; * `finset.subset_univ`: add `@[simp]`; * `card_finset_fin_le`, `fintype.card_finset_len`, `fin.prod_const` : new lemmas; * `order_iso.refl`: new definition.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
fin.heq_fun_iff: useSort*instead ofType*;fin.cast_refl: takeh : n = n := rflas an argument;fin.cast_to_equiv,fin.cast_eq_cast: relatefin.castto_root_.cast;finset.map_cast_heq: new lemma;finset.subset_univ: add@[simp];card_finset_fin_le,fintype.card_finset_len,fin.prod_const: new lemmas;order_iso.refl: new definition.