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 | |
| 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.
| -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 //. |