diff options
| author | Cyril Cohen | 2019-11-27 18:47:27 +0100 |
|---|---|---|
| committer | GitHub | 2019-11-27 18:47:27 +0100 |
| commit | cbc1688d9447860a60cb3ede83099a10bcd408e2 (patch) | |
| tree | 2471481f9a004a03d5b96c28ebaf1ee7e2f06e19 /mathcomp/ssreflect/binomial.v | |
| parent | 8b78152ce646d0f2f91b7c90f204dd98ef6a1d4b (diff) | |
| parent | 4bd5ba38e4f6c6456a8fcc39364a67b51fde92f2 (diff) | |
Merge pull request #441 from ggonthier/big_enum
Big enum
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 8bdb426..1649a89 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -386,8 +386,8 @@ rewrite -card_uniq_tuples. have bijFF: {on (_ : pred _), bijective (@Finfun D T)}. by exists fgraph => x _; [apply: FinfunK | apply: fgraphK]. rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t. -rewrite !inE -(big_andE predT) -big_filter big_all -all_map. -by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK. +rewrite !inE -(big_andE predT) -big_image /= big_all. +by rewrite -[t in RHS]FinfunK -codom_ffun. Qed. Lemma card_inj_ffuns D T : |