diff options
| author | Cyril Cohen | 2020-10-30 18:50:56 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 18:50:56 +0100 |
| commit | 1ec04efdcd1b00a6ae651551699c8b815a2a063f (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/character/mxrepresentation.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
| parent | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (diff) | |
Merge pull request #607 from pi8027/distr-suffixes
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/character/mxrepresentation.v')
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 51d28f8..e94e69f 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -4908,8 +4908,7 @@ Proof. rewrite map_kermx //; congr (kermx _); apply: map_lin1_mx => //= v. rewrite map_mxvec map_mxM; congr (mxvec (_ *m _)); last first. by apply: map_lin1_mx => //= u; rewrite map_mxM map_vec_mx. -apply/row_matrixP=> i. -by rewrite -map_row !rowK map_mxvec map_mx_sub map_mx1. +by apply/row_matrixP=> i; rewrite -map_row !rowK map_mxvec map_mxB map_mx1. Qed. Lemma rcent_map A : rcent rGf A^f = rcent rG A. @@ -4990,7 +4989,7 @@ rewrite {1}in_submodE mulmxA -in_submodE -in_submodJ; last first. by rewrite genmxE -(in_factmod_addsK _ V^f) submxMr. congr (in_submod _ _); rewrite -in_factmodJ // in_factmodE mulmxA -in_factmodE. apply/eqP; rewrite -subr_eq0 -def_rGf -!map_mxM -linearB in_factmod_eq0. -rewrite -map_mx_sub map_submx -in_factmod_eq0 linearB. +rewrite -map_mxB map_submx -in_factmod_eq0 linearB. rewrite /= (in_factmodJ modU) // val_factmodK. rewrite [valUV]val_factmodE mulmxA -val_factmodE val_factmodK. rewrite -val_submodE in_submodK ?subrr //. |