diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/solvable/center.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/solvable/center.v')
| -rw-r--r-- | mathcomp/solvable/center.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index d63c302..54726be 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -70,7 +70,7 @@ Canonical center_pgFun := [pgFun by morphim_center]. Section Center. Variables gT : finGroupType. -Implicit Type rT : finGroupType. +Implicit Type rT : finGroupType. Implicit Types (x y : gT) (A B : {set gT}) (G H K D : {group gT}). Lemma subcentP A B x : reflect (x \in A /\ centralises x B) (x \in 'C_A(B)). @@ -101,7 +101,7 @@ Proof. exact: subcentP. Qed. Lemma center_sub A : 'Z(A) \subset A. Proof. exact: subsetIl. Qed. -Lemma center1 : 'Z(1) = 1 :> {set gT}. +Lemma center1 : 'Z(1) = 1 :> {set gT}. Proof. exact: gF1. Qed. Lemma centerC A : {in A, centralised 'Z(A)}. @@ -338,7 +338,7 @@ Proof. transitivity ('ker (subg [group of setX H K / kerHK] \o coset kerHK)). rewrite /ker /morphpre /= /in_cprod /cprod_by; case: cprod_by_key => /=. by rewrite ['N(_) :&: _]quotientGK ?sub_center_normal ?ker_cprod_by_central. -by rewrite ker_comp ker_subg -kerE ker_coset. +by rewrite ker_comp ker_subg -kerE ker_coset. Qed. Lemma cpairg1_dom : H \subset 'dom (in_cprod \o @pairg1 gTH gTK). |