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/algebra/vector.v | |
| parent | 8b78152ce646d0f2f91b7c90f204dd98ef6a1d4b (diff) | |
| parent | 4bd5ba38e4f6c6456a8fcc39364a67b51fde92f2 (diff) | |
Merge pull request #441 from ggonthier/big_enum
Big enum
Diffstat (limited to 'mathcomp/algebra/vector.v')
| -rw-r--r-- | mathcomp/algebra/vector.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 87ca0f4..1f8ad30 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1879,7 +1879,7 @@ Variable (K : fieldType) (vT : vectType K). Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT}) (defV : V = (\sum_(i | P i) Vs i)%VS) : v \in V -> \sum_(i | P i) sumv_pi_for defV i v = v :> vT. -Proof. by apply: sumv_pi_uniq_sum; apply: enum_uniq. Qed. +Proof. by apply: sumv_pi_uniq_sum; have [e _ []] := big_enumP. Qed. Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT}) (defV : V = (\sum_(m <= i < n | P i) Vs i)%VS) : |