diff options
| author | Cyril Cohen | 2019-04-01 19:55:26 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-01 19:55:26 +0200 |
| commit | 9209c4414b22ead6b5a70d6f2bfb460b1ad26728 (patch) | |
| tree | b48d2702f2e5427683854d8f97b29c6948dad0d2 /mathcomp/solvable | |
| parent | 850862dc6475bd48524a294651400df4b5b7ecf3 (diff) | |
| parent | 0f785cb80a555ce4109255819becb953a968cc8c (diff) | |
Merge pull request #294 from math-comp/dependent-positive-finfun
Dependent positive finfun
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 10cbbaa..f5f3719 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -686,21 +686,21 @@ move=> p; rewrite inE. by do ?case/orP; move/eqP=> <- a; rewrite !(permM, permE); case: a; do 6?case. Qed. -Definition sop (p : {perm cube}) : seq cube := val (val (val p)). +Definition sop (p : {perm cube}) : seq cube := fgraph (val p). Lemma sop_inj : injective sop. -Proof. by do 2!apply: (inj_comp val_inj); apply: val_inj. Qed. +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. Proof. -move=> x y i; rewrite permM -!sop_spec (nth_map F0) // size_tuple /=. +move=> x y i; rewrite permM -!sop_spec [RHS](nth_map F0) // size_tuple /=. by rewrite card_ord ltn_ord. Qed. |