diff options
| author | Cyril Cohen | 2020-11-19 18:33:21 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-19 21:38:46 +0100 |
| commit | e565f8d9bebd4fd681c34086d5448dbaebc11976 (patch) | |
| tree | 3e74907bf8e310b6400b7c340357ad44fc44a83f /mathcomp/solvable/primitive_action.v | |
| parent | 0dbefe01e54a467b7932a514355f0435b4cfb978 (diff) | |
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/solvable/primitive_action.v')
| -rw-r--r-- | mathcomp/solvable/primitive_action.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 80005a4..27c0780 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -120,7 +120,7 @@ have [trG _] := andP primG; have [x Sx defS] := imsetP trG. move: primG; rewrite (trans_prim_astab Sx) // => /maximal_eqP[_]. case/(_ ('C_G[x | to] <*> H)%G) => /= [||cxH|]; first exact: joing_subl. - by rewrite join_subG subsetIl. -- have{cxH} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr. +- have{} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr. rewrite subsetI sHG /= in cxH; left; apply/subsetP=> a Ha. apply/astabP=> y Sy; have [b Gb ->] := atransP2 trG Sx Sy. rewrite actCJV [to x (a ^ _)](astab1P _) ?(subsetP cxH) //. |