diff options
| author | Georges Gonthier | 2018-12-04 13:27:53 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-04 13:27:53 +0100 |
| commit | e99b8b9695cdb53492e63077cb0dd551c4a06dc3 (patch) | |
| tree | 9af429f5d53b30de0c44e11ed651403289f39108 /mathcomp/solvable/maximal.v | |
| parent | 03ad994dfee48e1a7b2b7091c45dfdcf4402f826 (diff) | |
| parent | 8c82657e7692049dde4a4c44a2ea53d0c4fa7cb5 (diff) | |
Merge pull request #253 from anton-trunov/arguments
Document parameter names whenever possible
Diffstat (limited to 'mathcomp/solvable/maximal.v')
| -rw-r--r-- | mathcomp/solvable/maximal.v | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 5f7a9ed..781abbe 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -102,16 +102,14 @@ Definition SCN_at n B := [set A in SCN B | n <= 'r(A)]. End Defs. -Arguments charsimple _ _%g. -Arguments Frattini _ _%g. -Arguments Fitting _ _%g. -Arguments critical _ _%g _%g. -Arguments special _ _%g. -Arguments extraspecial _ _%g. -Arguments SCN _ _%g. -Arguments SCN_at _ _%N _%g. - -Prenex Implicits maximal simple charsimple critical special extraspecial. +Arguments charsimple {gT} A%g. +Arguments Frattini {gT} A%g. +Arguments Fitting {gT} A%g. +Arguments critical {gT} A%g B%g. +Arguments special {gT} A%g. +Arguments extraspecial {gT} A%g. +Arguments SCN {gT} B%g. +Arguments SCN_at {gT} n%N B%g. Notation "''Phi' ( A )" := (Frattini A) (at level 8, format "''Phi' ( A )") : group_scope. @@ -459,7 +457,7 @@ Section FittingFun. Implicit Types gT rT : finGroupType. -Lemma morphim_Fitting : GFunctor.pcontinuous Fitting. +Lemma morphim_Fitting : GFunctor.pcontinuous (@Fitting). Proof. move=> gT rT G D f; apply: Fitting_max. by rewrite morphim_normal ?Fitting_normal. |