diff options
Diffstat (limited to 'mathcomp/solvable/frobenius.v')
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index 3416587..eb7ceab 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -98,17 +98,15 @@ CoInductive has_Frobenius_action G H : Prop := End Definitions. -Arguments Scope semiregular [_ group_scope group_scope]. -Arguments Scope semiprime [_ group_scope group_scope]. -Arguments Scope normedTI [_ group_scope group_scope group_scope]. -Arguments Scope Frobenius_group_with_complement [_ group_scope group_scope]. -Arguments Scope Frobenius_group [_ group_scope]. -Arguments Scope Frobenius_group_with_kernel [_ group_scope group_scope]. -Arguments Scope Frobenius_group_with_kernel_and_complement - [_ group_scope group_scope group_scope]. -Arguments Scope Frobenius_action - [_ group_scope group_scope _ group_scope action_scope]. -Arguments Scope has_Frobenius_action [_ group_scope group_scope]. +Arguments semiregular _ _%g _%g. +Arguments semiprime _ _%g _%g. +Arguments normedTI _ _%g _%g _%g. +Arguments Frobenius_group_with_complement _ _%g _%g. +Arguments Frobenius_group _ _%g. +Arguments Frobenius_group_with_kernel _ _%g _%g. +Arguments Frobenius_group_with_kernel_and_complement _ _%g _%g _%g. +Arguments Frobenius_action _ _%g _%g _ _%g _%act. +Arguments has_Frobenius_action _ _%g _%g. Notation "[ 'Frobenius' G 'with' 'complement' H ]" := (Frobenius_group_with_complement G H) |