diff options
| author | Enrico Tassi | 2020-11-23 13:39:15 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-23 13:39:15 +0100 |
| commit | e6a25b8d4806cf968dbf6c33343ba1d1fb28ddf6 (patch) | |
| tree | f4010c0e566303cbc42b4b15f989a02651e549c1 /mathcomp/character | |
| parent | d954da5acab8c1ed0786f05766e2161b5c09bcca (diff) | |
| parent | 1c03fed9bd5ab57b99405802f17d50ff0888f887 (diff) | |
Merge pull request #667 from CohenCyril/ssrcoq8.10
Using Coq 8.10 ssreflect new features
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index ea93ab2..ad16989 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -5687,9 +5687,9 @@ elim: t => //=. - by move=> k _; apply/rowP=> i; rewrite !mxE /= nth_row_env nth_map_rVval. - by move=> x _; rewrite eval_mx_term. - by move=> x _; rewrite eval_mx_term. -- move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite -{}IH1 // -{}IH2 //. +- move=> t1 + t2 + /andP[rt1 rt2] => <-// <-//. by apply/rowP=> k; rewrite !mxE. -- by move=> t1 IH1 rt1; rewrite -{}IH1 //; apply/rowP=> k; rewrite !mxE. +- by move=> t1 + rt1 => <-//; apply/rowP=> k; rewrite !mxE. - move=> t1 IH1 n1 rt1; rewrite eval_mulmx eval_mx_term mul_scalar_mx. by rewrite scaler_nat {}IH1 //; elim: n1 => //= n1 IHn1; rewrite !mulrS IHn1. - by move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite eval_mulT IH1 ?IH2. |