diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/finalg.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 3 |
2 files changed, 4 insertions, 9 deletions
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index ac3a74e..9c0025b 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -125,7 +125,9 @@ Coercion countType : type >-> Countable.type. Canonical countType. Coercion finType : type >-> Finite.type. Canonical finType. +Coercion baseFinGroupType : type >-> FinGroup.base_type. Canonical baseFinGroupType. +Coercion finGroupType : type >-> FinGroup.type. Canonical finGroupType. Coercion zmodType : type >-> GRing.Zmodule.type. Canonical zmodType. @@ -645,13 +647,9 @@ Definition countComUnitRing_finComRingType := @ComRing.Pack countComUnitRingType xclass. Definition countComUnitRing_finUnitRingType := @UnitRing.Pack countComUnitRingType xclass. -Definition unitRing_countComRingType := - @CountRing.ComRing.Pack unitRingType xclass. Definition unitRing_finComRingType := @ComRing.Pack unitRingType xclass. Definition countUnitRing_finComRingType := @ComRing.Pack countUnitRingType xclass. -Definition comRing_countUnitRingType := - @CountRing.UnitRing.Pack comRingType xclass. Definition comRing_finUnitRingType := @UnitRing.Pack comRingType xclass. Definition countComRing_finUnitRingType := @UnitRing.Pack countComRingType xclass. @@ -720,10 +718,8 @@ Canonical countComUnitRing_finZmodType. Canonical countComUnitRing_finRingType. Canonical countComUnitRing_finComRingType. Canonical countComUnitRing_finUnitRingType. -Canonical unitRing_countComRingType. Canonical unitRing_finComRingType. Canonical countUnitRing_finComRingType. -Canonical comRing_countUnitRingType. Canonical comRing_finUnitRingType. Canonical countComRing_finUnitRingType. Canonical finComRing_finUnitRingType. @@ -1231,7 +1227,6 @@ Definition lalg_finZmodType := @Zmodule.Pack lalgType xclass. Definition lalg_finLmodType := @Lmodule.Pack R phR lalgType xclass. Definition lalg_countRingType := @CountRing.Ring.Pack lalgType xclass. Definition lalg_finRingType := @Ring.Pack lalgType xclass. -Definition lmod_ringType := @GRing.Ring.Pack lmodType xclass. Definition lmod_countRingType := @CountRing.Ring.Pack lmodType xclass. Definition lmod_finRingType := @Ring.Pack lmodType xclass. Definition finLmod_ringType := @GRing.Ring.Pack finLmodType xclass. @@ -1285,7 +1280,6 @@ Canonical lalg_finZmodType. Canonical lalg_finLmodType. Canonical lalg_countRingType. Canonical lalg_finRingType. -Canonical lmod_ringType. Canonical lmod_countRingType. Canonical lmod_finRingType. Canonical finLmod_ringType. 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 |