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/character | |
| parent | 850862dc6475bd48524a294651400df4b5b7ecf3 (diff) | |
| parent | 0f785cb80a555ce4109255819becb953a968cc8c (diff) | |
Merge pull request #294 from math-comp/dependent-positive-finfun
Dependent positive finfun
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/character.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/integral_char.v | 2 |
2 files changed, 5 insertions, 3 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/character/integral_char.v b/mathcomp/character/integral_char.v index 3c2b0d6..d73f938 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -423,7 +423,7 @@ Theorem dvd_irr1_index_center gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G : 'Z('chi_i)%CF|)%C. Proof. without loss fful: gT G i / cfaithful 'chi_i. - rewrite -{2}[i](quo_IirrK _ (subxx _)) ?mod_IirrE ?cfModE ?cfker_normal //. + rewrite -{2}[i](quo_IirrK _ (subxx _)) 1?mod_IirrE ?cfModE ?cfker_normal //. rewrite morph1; set i1 := quo_Iirr _ i => /(_ _ _ i1) IH. have fful_i1: cfaithful 'chi_i1. by rewrite quo_IirrE ?cfker_normal ?cfaithful_quo. |