diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 34c1c7c..f5f3719 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -694,8 +694,8 @@ Proof. by move=> p1 p2 /val_inj/(can_inj fgraphK)/val_inj. Qed. Definition prod_tuple (t1 t2 : seq cube) := map (fun n : 'I_6 => nth F0 t2 n) t1. -Lemma sop_spec : forall x (n0 : 'I_6), nth F0 (sop x) n0 = x n0. -Proof. by move=> x n0; rewrite -pvalE unlock enum_rank_ord (tnth_nth F0). Qed. +Lemma sop_spec x (n0 : 'I_6): nth F0 (sop x) n0 = x n0. +Proof. by rewrite nth_fgraph_ord pvalE. Qed. Lemma prod_t_correct : forall (x y : {perm cube}) (i : cube), (x * y) i = nth F0 (prod_tuple (sop x) (sop y)) i. |