diff options
| author | Kazuhiko Sakaguchi | 2019-04-05 19:09:06 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-04-06 00:04:44 +0200 |
| commit | 407b4c412d4a1324450d01fa09a41aad7673b1bf (patch) | |
| tree | 262a9689d6c6c259d53b2a0c85198d5953d39aee /mathcomp/solvable | |
| parent | 7583b9007c3ed23720d26a522f0d822722a11e2a (diff) | |
Fix inheritance bugs in finalg and extremal
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 |