diff options
| author | Cyril Cohen | 2020-11-19 20:37:16 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-20 12:10:46 +0100 |
| commit | 1c03fed9bd5ab57b99405802f17d50ff0888f887 (patch) | |
| tree | cdb93a0167e600545119a390ee1f055265c00264 /mathcomp/character | |
| parent | 75da4dbbf2fa6ca6ee150d272d3a793bff63c931 (diff) | |
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 e94e69f..4202c6e 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -5684,9 +5684,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. |