diff options
| author | Cyril Cohen | 2019-04-08 14:18:00 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-08 14:18:00 +0200 |
| commit | 86d0a640383d6039302b9126620d0bf031a2a011 (patch) | |
| tree | f81a6cfe987fcd2944f9df1566a6059408761cf6 /mathcomp/solvable | |
| parent | 8099c05ca650b12abd0fbaf676357e86fd175a8a (diff) | |
| parent | a348deb229074be37ff31fd892a7d8835a49b566 (diff) | |
Merge pull request #318 from CohenCyril/hierarchy_test
Least common childen
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/extremal.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 9ac5236..a51fe9c 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -1533,7 +1533,8 @@ Canonical extremal_group_countType := CountType _ extremal_group_countMixin. Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6. Proof. by case: c. Qed. Definition extremal_group_finMixin := Finite.CountMixin bound_extremal_groups. -Canonical extremal_group_finType := FinType _ extremal_group_finMixin. +Canonical extremal_group_finType := + FinType extremal_group_type extremal_group_finMixin. Definition extremal_class (A : {set gT}) := let m := #|A| in let p := pdiv m in let n := logn p m in |