diff options
| author | Maxime Dénès | 2017-11-06 17:15:35 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-06 17:18:44 +0100 |
| commit | c2a42557d0cc7c4c776a4572dcfeef011bfc73b8 (patch) | |
| tree | 9435d7ddc76abb74b7df0eec7abf861048dc89a2 /mathcomp/odd_order | |
| parent | 7110a6e302fe102b6fb8df675511a44d8441d6c5 (diff) | |
Fix the only remaining spurious injection in the entire codebase.
We may want to make it an error, now that the transition period has been
long enough.
Diffstat (limited to 'mathcomp/odd_order')
| -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 //. |