diff options
| author | Cyril Cohen | 2020-10-30 18:50:56 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 18:50:56 +0100 |
| commit | 1ec04efdcd1b00a6ae651551699c8b815a2a063f (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/character/inertia.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
| parent | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (diff) | |
Merge pull request #607 from pi8027/distr-suffixes
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/character/inertia.v')
| -rw-r--r-- | mathcomp/character/inertia.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 76535fa..29d7162 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -1492,7 +1492,7 @@ have kerN_mu_t: N \subset cfker (mu / 'chi_t)%R. by rewrite /= uNlam tNlam divrr ?lin_char_unitr ?cfker_cfun1. have co_e_mu_t: coprime e #[(mu / 'chi_t)%R]%CF. suffices dv_o_mu_t: #[(mu / 'chi_t)%R]%CF %| 'o(mu)%CF * 'o('chi_t)%CF. - by rewrite (coprime_dvdr dv_o_mu_t) // coprime_mulr o_mu co_e_lam. + by rewrite (coprime_dvdr dv_o_mu_t) // coprimeMr o_mu co_e_lam. rewrite !cfDet_order_lin //; apply/dvdn_cforderP=> x Gx. rewrite invr_lin_char // !cfunE exprMn -rmorphX {2}mulnC. by rewrite !(dvdn_cforderP _) ?conjC1 ?mulr1 // dvdn_mulr. @@ -1513,7 +1513,7 @@ Corollary extend_solvable_coprime_irr G N t (theta := 'chi[N]_t) : d = c]. Proof. set e := #|G : N|; set f := truncC _ => nsNG solG IGtheta. -rewrite coprime_mulr => /andP[co_e_th co_e_f]. +rewrite coprimeMr => /andP[co_e_th co_e_f]. have [sNG nNG] := andP nsNG; pose lambda := cfDet theta. have lin_lam: lambda \is a linear_char := cfDet_lin_char theta. have IGlam: G \subset 'I[lambda]. |