diff options
| author | Christian Doczkal | 2020-09-10 18:15:25 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-09-29 11:10:31 +0200 |
| commit | 5b31a9e767694ce134fdff4461a876411eba0f2d (patch) | |
| tree | 3cccd5964f214d314aca7f77a1742b9d57245ef0 /mathcomp/solvable/maximal.v | |
| parent | 298830c5a3860c7a645df6effe7d1cc228d56150 (diff) | |
rename mem_imset2 to imset2_f (with deprecation)
Diffstat (limited to 'mathcomp/solvable/maximal.v')
| -rw-r--r-- | mathcomp/solvable/maximal.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 5af62c9..3786cff 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1544,7 +1544,7 @@ have{genXp minU xp1 sVU ltVU} expVp: exponent V %| p. have{A pA defA1 sX'A V expVp} Zxy: [~ x, y] \in Z. rewrite -defA1 (OhmE 1 pA) mem_gen // !inE (exponentP expVp). by rewrite (subsetP sX'A) //= mem_commg ?(subsetP sUX). - by rewrite groupMl -1?[x^-1]conjg1 mem_gen // mem_imset2 // ?groupV cycle_id. + by rewrite groupMl -1?[x^-1]conjg1 mem_gen // imset2_f // ?groupV cycle_id. have{Zxy sUX cZX} cXYxy: [~ x, y] \in 'C(XY). by rewrite centsC in cZX; rewrite defXY (subsetP (centS sUX)) ?(subsetP cZX). rewrite -defU1 exponent_Ohm1_class2 // nil_class2 -defXY der1_joing_cycles //. |