diff options
| -rw-r--r-- | mathcomp/character/character.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 41 |
2 files changed, 25 insertions, 22 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 783c46f..eda6f5a 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -667,11 +667,13 @@ Proof. by rewrite eqr_le ltr_geF ?irr1_gt0. Qed. Lemma irr_neq0 i : 'chi_i != 0. Proof. by apply: contraNneq (irr1_neq0 i) => ->; rewrite cfunE. Qed. -Definition cfIirr B (chi : 'CF(B)) : Iirr B := inord (index chi (irr B)). +Local Remark cfIirr_key : unit. Proof. by []. Qed. +Definition cfIirr : forall B, 'CF(B) -> Iirr B := + locked_with cfIirr_key (fun B chi => inord (index chi (irr B))). Lemma cfIirrE chi : chi \in irr G -> 'chi_(cfIirr chi) = chi. Proof. -move=> chi_irr; rewrite (tnth_nth 0) inordK ?nth_index //. +move=> chi_irr; rewrite (tnth_nth 0) [cfIirr]unlock inordK ?nth_index //. by rewrite -index_mem size_tuple in chi_irr. Qed. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 9a8c723..db03671 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -239,34 +239,35 @@ Notation family F := (family_mem (fmem F)). Section InheritedStructures. Variable aT : finType. +Notation dffun_aT rT rS := {dffun forall x : aT, rT x : rS}. -Definition finfun_eqMixin (rT : _ -> eqType) := - @PcanEqMixin {dffun finPi aT rT} _ _ _ tfgraphK. +Local Remark eqMixin rT : Equality.mixin_of (dffun_aT rT eqType). +Proof. exact: PcanEqMixin tfgraphK. Qed. Canonical finfun_eqType (rT : eqType) := - EqType {ffun aT -> rT} (finfun_eqMixin _). -Canonical dfinfun_eqType (rT : _ -> eqType) := - EqType {dffun finPi aT rT} (finfun_eqMixin _). + EqType {ffun aT -> rT} (eqMixin (fun=> rT)). +Canonical dfinfun_eqType rT := + EqType (dffun_aT rT eqType) (eqMixin rT). -Definition finfun_choiceMixin (rT : _ -> choiceType) := - @PcanChoiceMixin _ {dffun finPi aT rT} _ _ tfgraphK. +Local Remark choiceMixin rT : Choice.mixin_of (dffun_aT rT choiceType). +Proof. exact: PcanChoiceMixin tfgraphK. Qed. Canonical finfun_choiceType (rT : choiceType) := - ChoiceType {ffun aT -> rT} (finfun_choiceMixin _). -Canonical dfinfun_choiceType (rT : _ -> choiceType) := - ChoiceType {dffun finPi aT _} (finfun_choiceMixin rT). + ChoiceType {ffun aT -> rT} (choiceMixin (fun=> rT)). +Canonical dfinfun_choiceType rT := + ChoiceType (dffun_aT rT choiceType) (choiceMixin rT). -Definition finfun_countMixin (rT : _ -> countType) := - @PcanCountMixin _ {dffun finPi aT rT} _ _ tfgraphK. +Local Remark countMixin rT : Countable.mixin_of (dffun_aT rT countType). +Proof. exact: PcanCountMixin tfgraphK. Qed. Canonical finfun_countType (rT : countType) := - CountType {ffun aT -> rT} (finfun_countMixin _). -Canonical dfinfun_countType (rT : _ -> countType) := - CountType {dffun finPi aT rT} (finfun_countMixin _). + CountType {ffun aT -> rT} (countMixin (fun => rT)). +Canonical dfinfun_countType rT := + CountType (dffun_aT rT countType) (countMixin rT). -Definition finfun_finMixin (rT : _ -> finType) := - @PcanFinMixin (dfinfun_countType rT) _ _ _ tfgraphK. +Local Definition finMixin rT := + PcanFinMixin (tfgraphK : @pcancel _ (dffun_aT rT finType) _ _). Canonical finfun_finType (rT : finType) := - FinType {ffun aT -> rT} (finfun_finMixin _). -Canonical dfinfun_finType (rT : _ -> finType) := - FinType {dffun finPi aT rT} (finfun_finMixin _). + FinType {ffun aT -> rT} (finMixin (fun=> rT)). +Canonical dfinfun_finType rT := + FinType (dffun_aT rT finType) (finMixin rT). End InheritedStructures. |