diff options
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 |