diff options
| author | Kazuhiko Sakaguchi | 2020-10-09 00:21:00 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-29 12:31:31 +0900 |
| commit | c6e0d703165b0c60c270672eb542aa8934929bfe (patch) | |
| tree | 3ce1b05b861ca60e88bc7ab8b5226b12a879e3e6 /mathcomp/character/mxrepresentation.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
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 //. |