diff options
| author | Georges Gonthier | 2019-05-06 18:04:48 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-06 18:04:48 +0200 |
| commit | 02830d7cf24f9198d5e7cb81843d6ca5cb69f68a (patch) | |
| tree | 73e8bf66926855dc2d0a440f6a6a0c97a92344b3 /mathcomp/character/classfun.v | |
| parent | a3f3d1aead4b5c35fb4a74be1cca7a5cde253d9a (diff) | |
| parent | b59653a5b377f91a21e8036bf0b5d98a35fc4963 (diff) | |
Merge pull request #342 from math-comp/deprecation
add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names
Diffstat (limited to 'mathcomp/character/classfun.v')
| -rw-r--r-- | mathcomp/character/classfun.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 468aa66..65167b5 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -2412,7 +2412,7 @@ Proof. set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS. have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj). have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS. -have [|eqSuS _] := leq_size_perm uniqSu sSuS; first by rewrite size_map. +have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map. by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)). Qed. |