diff options
Diffstat (limited to 'mathcomp/character/character.v')
| -rw-r--r-- | mathcomp/character/character.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index a657fa5..9a61ebe 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -576,7 +576,7 @@ Proof. by move=> i; rewrite /irr_of_socle enum_valK cast_ordK addrK. Qed. Lemma irr_of_socleK : cancel irr_of_socle W. Proof. by move=> Wi; rewrite /W subrK cast_ordKV enum_rankK. Qed. -Hint Resolve socle_of_IirrK irr_of_socleK. +Hint Resolve socle_of_IirrK irr_of_socleK : core. Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}. Proof. by apply: onW_bij; exists W. Qed. |