diff options
| author | Enrico | 2017-11-06 19:07:09 +0100 |
|---|---|---|
| committer | GitHub | 2017-11-06 19:07:09 +0100 |
| commit | 1e7a80cc115a2a4f284a2a9c33e56f55687a764e (patch) | |
| tree | 9435d7ddc76abb74b7df0eec7abf861048dc89a2 /mathcomp | |
| parent | 7110a6e302fe102b6fb8df675511a44d8441d6c5 (diff) | |
| parent | c2a42557d0cc7c4c776a4572dcfeef011bfc73b8 (diff) | |
Merge pull request #154 from maximedenes/nothing-to-inject
Fix the only remaining spurious injection in the entire codebase.
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/odd_order/PFsection14.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/odd_order/PFsection14.v b/mathcomp/odd_order/PFsection14.v index c634ec1..bed35bc 100644 --- a/mathcomp/odd_order/PFsection14.v +++ b/mathcomp/odd_order/PFsection14.v @@ -349,7 +349,7 @@ have o1M: orthonormal (map tau1M calM). have Lgt1: (1 < size calL)%N by apply: seqInd_nontrivial (mFT_odd _ ) _ Lphi. have [[_ _]] := Dade_Ind1_sub_lin cohL Lgt1 irr_phi Lphi phi1. rewrite -/tauL -/betaL -/calL => ZbetaL [Gamma [_ _ [b _ Dbeta]]]. -rewrite odd_Frobenius_index_ler ?mFT_odd // -/u => -[]// [_ ub_Ga] _ nz_a. +rewrite odd_Frobenius_index_ler ?mFT_odd // -/u => -[]// _ ub_Ga _ nz_a. have Za: a \in Cint by rewrite Cint_cfdot_vchar // ?Ztau1 ?mem_zchar. have [X M_X [Del [defGa oXD oDM]]] := orthogonal_split (map tau1M calM) Gamma. apply: ler_trans ub_Ga; rewrite defGa cfnormDd // ler_paddr ?cfnorm_ge0 //. |