diff options
| author | Christian Doczkal | 2020-09-10 17:45:57 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-09-29 11:10:31 +0200 |
| commit | 298830c5a3860c7a645df6effe7d1cc228d56150 (patch) | |
| tree | a9a97a1ba6abd46f94d5ca48ece171cc9d88df2f /mathcomp/character/integral_char.v | |
| parent | 7a34bf388b368b450f20a7e10e5a3076370d2d52 (diff) | |
rename mem_imset to imset_f (with deprecation)
Diffstat (limited to 'mathcomp/character/integral_char.v')
| -rw-r--r-- | mathcomp/character/integral_char.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 2b886a6..c603f91 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -465,9 +465,9 @@ transitivity ('chi_i x * 'chi_i (x^-1)%g *+ #|h x|); last first. by rewrite mulf_neq0 // lin_char_neq0 /= ?cfcenter_fful_irr. rewrite -[z](mulKg u) -cGz // -conjMg /h classGidl {u Gu}//. apply/eqP/setP=> w; apply/mulsgP/mulsgP=> [][_ z1 /imsetP[v Gv ->] Zz1 ->]. - exists (x ^ v)%g (z * z1)%g; rewrite ?mem_imset ?groupM //. + exists (x ^ v)%g (z * z1)%g; rewrite ?imset_f ?groupM //. by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg. - exists ((x * z) ^ v)%g (z^-1 * z1)%g; rewrite ?mem_imset ?groupM ?groupV //. + exists ((x * z) ^ v)%g (z^-1 * z1)%g; rewrite ?imset_f ?groupM ?groupV //. by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg mulKVg. rewrite !irr_inv DchiZ ?groupJ ?cfunJ // rmorphM mulrACA -!normCK -exprMn. by rewrite (normC_lin_char lin_lambda) ?mulr1 //= cfcenter_fful_irr. |