diff options
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. |