diff options
| author | Christian Doczkal | 2020-09-10 18:15:25 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-09-29 11:10:31 +0200 |
| commit | 5b31a9e767694ce134fdff4461a876411eba0f2d (patch) | |
| tree | 3cccd5964f214d314aca7f77a1742b9d57245ef0 /mathcomp/character | |
| parent | 298830c5a3860c7a645df6effe7d1cc228d56150 (diff) | |
rename mem_imset2 to imset2_f (with deprecation)
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/vcharacter.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index faecc02..e1c7ec4 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -696,7 +696,7 @@ have [j def_chi_j]: {j | 'chi_j = phi}. exists j; rewrite ?cfkerEirr def_chi_j //; apply/subsetP => x /setDP[Gx notHx]. rewrite inE cfunE def_phi // cfunE -/a cfun1E // Gx mulr1 cfIndE //. rewrite big1 ?mulr0 ?add0r // => y Gy; apply/theta0/(contra _ notHx) => Hxy. -by rewrite -(conjgK y x) cover_imset -class_supportEr mem_imset2 ?groupV. +by rewrite -(conjgK y x) cover_imset -class_supportEr imset2_f ?groupV. Qed. End MoreVchar. |