aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/odd_order
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/odd_order')
-rw-r--r--mathcomp/odd_order/BGappendixC.v11
-rw-r--r--mathcomp/odd_order/PFsection11.v2
-rw-r--r--mathcomp/odd_order/PFsection3.v2
-rw-r--r--mathcomp/odd_order/PFsection5.v8
-rw-r--r--mathcomp/odd_order/PFsection6.v6
-rw-r--r--mathcomp/odd_order/PFsection7.v2
6 files changed, 16 insertions, 15 deletions
diff --git a/mathcomp/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v
index a64c49a..16a0a3c 100644
--- a/mathcomp/odd_order/BGappendixC.v
+++ b/mathcomp/odd_order/BGappendixC.v
@@ -288,7 +288,7 @@ Proof.
have [q_gt4 | q_le4] := ltnP 4 q.
pose inK x := enum_rank_in (classes1 H) (x ^: H).
have inK_E x: x \in H -> enum_val (inK x) = x ^: H.
- by move=> Hx; rewrite enum_rankK_in ?mem_classes.
+ by move=> Hx; rewrite enum_rankK_in ?mem_classes.
pose j := inK s; pose k := inK (s ^+ 2)%g; pose e := gring_classM_coef j j k.
have cPP: abelian P by rewrite -(injm_abelian inj_sigma) ?zmod_abelian.
have Hs: s \in H by rewrite -(sdprodW defH) -[s]mulg1 mem_mulg.
@@ -355,18 +355,19 @@ have [q_gt4 | q_le4] := ltnP 4 q.
by rewrite sub_cent1 groupX // (subsetP cPP).
rewrite mulrnA -second_orthogonality_relation ?groupX // big_mkcond.
by apply: ler_sum => i _; rewrite normCK; case: ifP; rewrite ?mul_conjC_ge0.
- have sqrtP_gt0: 0 < sqrtC #|P|%:R by rewrite sqrtC_gt0 ?gt0CG.
- have{De ub_linH'}: `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R.
+ have sqrtP_gt0: 0 < sqrtC #|P|%:R :> algC by rewrite sqrtC_gt0 ?gt0CG.
+ have{De ub_linH'}:
+ `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R :> algC.
rewrite natrM De mulrCA mulrA divfK ?neq0CG // (bigID linH) /= sum_linH.
rewrite mulrDr addrC addKr mulrC mulr_suml /chi_s2.
rewrite (ler_trans (ler_norm_sum _ _ _)) // -ler_pdivr_mulr // mulr_suml.
apply: ler_trans (ub_linH' 1%N isT); apply: ler_sum => i linH'i.
rewrite ler_pdivr_mulr // degU ?divfK ?neq0CG //.
rewrite normrM -normrX norm_conjC ler_wpmul2l ?normr_ge0 //.
- rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK.
+ rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK.
apply: ler_trans (ub_linH' 2 isT); rewrite (bigD1 i) ?ler_paddr //=.
by apply: sumr_ge0 => i1 _; rewrite exprn_ge0 ?normr_ge0.
- rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _].
+ rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _].
rewrite -ltC_nat -(ltr_pmul2l (gt0CG P)) {lb_Pe}(ltr_le_trans _ lb_Pe) //.
rewrite ltr_subr_addl (@ler_lt_trans _ ((p ^ q.-1)%:R ^+ 2)) //; last first.
rewrite -!natrX ltC_nat ltn_sqr oU ltn_divRL ?dvdn_pred_predX //.
diff --git a/mathcomp/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v
index b966f25..3c4ec9f 100644
--- a/mathcomp/odd_order/PFsection11.v
+++ b/mathcomp/odd_order/PFsection11.v
@@ -232,7 +232,7 @@ Lemma bounded_proper_coherent H1 :
(#|HU : H1| <= 2 * q * #|U : C| + 1)%N.
Proof.
move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU.
-suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R.
+suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC.
rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM.
congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)).
rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC.
diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v
index cb55ae4..9011122 100644
--- a/mathcomp/odd_order/PFsection3.v
+++ b/mathcomp/odd_order/PFsection3.v
@@ -1360,7 +1360,7 @@ have{oxi_00} oxi_i0 i j i0: '[xi_ i j, xi_ i0 0] = ((i == i0) && (j == 0))%:R.
by rewrite cfdotC Xi0_X0j // conjC0.
have [-> | nzi2] := altP (i2 =P 0); first exact: oxi_0j.
have [-> | nzj2] := altP (j2 =P 0); first exact: oxi_i0.
-rewrite cfdotC eq_sym; apply: canLR conjCK _; rewrite rmorph_nat.
+rewrite cfdotC eq_sym; apply: canLR (@conjCK _) _; rewrite rmorph_nat.
have [-> | nzi1] := altP (i1 =P 0); first exact: oxi_0j.
have [-> | nzj1] := altP (j1 =P 0); first exact: oxi_i0.
have ->: xi_ i1 j1 = beta i1 j1 + xi_ i1 0 + xi_ 0 j1 by rewrite /xi_ !ifN.
diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v
index d318f5f..3f90da7 100644
--- a/mathcomp/odd_order/PFsection5.v
+++ b/mathcomp/odd_order/PFsection5.v
@@ -492,7 +492,7 @@ Definition subcoherent S tau R :=
(*c*) pairwise_orthogonal S,
(*d*) {in S, forall xi : 'CF(L : {set gT}),
[/\ {subset R xi <= 'Z[irr G]}, orthonormal (R xi)
- & tau (xi - xi^*)%CF = \sum_(alpha <- R xi) alpha]}
+ & tau (xi - xi^*%CF) = \sum_(alpha <- R xi) alpha]}
& (*e*) {in S &, forall xi phi : 'CF(L),
orthogonal phi (xi :: xi^*%CF) -> orthogonal (R phi) (R xi)}].
@@ -621,7 +621,7 @@ have isoS1: {in S1, isometry [eta tau with eta1 |-> zeta1], to 'Z[irr G]}.
split=> [xi eta | eta]; rewrite !in_cons /=; last first.
by case: eqP => [-> | _ /isoS[/Ztau/zcharW]].
do 2!case: eqP => [-> _|_ /isoS[? ?]] //; last exact: Itau.
- by apply/(can_inj conjCK); rewrite -!cfdotC.
+ by apply/(can_inj (@conjCK _)); rewrite -!cfdotC.
have [nu Dnu IZnu] := Zisometry_of_iso freeS1 isoS1.
exists nu; split=> // phi; rewrite zcharD1E => /andP[].
case/(zchar_expansion (free_uniq freeS1)) => b Zb {phi}-> phi1_0.
@@ -646,7 +646,7 @@ have N_S: {subset S <= character} by move=> _ /irrS/irrP[i ->]; apply: irr_char.
have Z_S: {subset S <= 'Z[irr L]} by move=> chi /N_S/char_vchar.
have o1S: orthonormal S by apply: sub_orthonormal (irr_orthonormal L).
have [[_ dotSS] oS] := (orthonormalP o1S, orthonormal_orthogonal o1S).
-pose beta chi := tau (chi - chi^*)%CF; pose eqBP := _ =P beta _.
+pose beta chi := tau (chi - chi^*%CF); pose eqBP := _ =P beta _.
have Zbeta: {in S, forall chi, chi - (chi^*)%CF \in 'Z[S, L^#]}.
move=> chi Schi; rewrite /= zcharD1E rpredB ?mem_zchar ?ccS //= !cfunE.
by rewrite subr_eq0 conj_Cnat // Cnat_char1 ?N_S.
@@ -885,7 +885,7 @@ Lemma subcoherent_norm chi psi (tau1 : {additive 'CF(L) -> 'CF(G)}) X Y :
[/\ chi \in S, psi \in 'Z[irr L] & orthogonal (chi :: chi^*)%CF psi] ->
let S0 := chi - psi :: chi - chi^*%CF in
{in 'Z[S0], isometry tau1, to 'Z[irr G]} ->
- tau1 (chi - chi^*)%CF = tau (chi - chi^*)%CF ->
+ tau1 (chi - chi^*%CF) = tau (chi - chi^*%CF) ->
[/\ tau1 (chi - psi) = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)] ->
[/\ (*a*) '[chi] <= '[X]
& (*b*) '[psi] <= '[Y] ->
diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v
index 6d9ecfc..cbde798 100644
--- a/mathcomp/odd_order/PFsection6.v
+++ b/mathcomp/odd_order/PFsection6.v
@@ -83,13 +83,13 @@ Lemma coherent_seqIndD_bound (A B C D : {group gT}) :
(*a*) [/\ A \proper K, B \subset D, D \subset C, C \subset K
& D / B \subset 'Z(C / B)]%g ->
(*b*) coherent (S A) L^# tau -> \unless coherent (S B) L^# tau,
- #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R.
+ #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R :> algC.
Proof.
move=> [nsAL nsBL nsCL nsDL] [ltAK sBD sDC sCK sDbZC] cohA.
have sBC := subset_trans sBD sDC; have sBK := subset_trans sBC sCK.
have [sAK nsBK] := (proper_sub ltAK, normalS sBK sKL nsBL).
have{sBC} [nsAK nsBC] := (normalS sAK sKL nsAL, normalS sBC sCK nsBK).
-rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n //.
+rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n ?ler01 //.
apply/unless_contra; rewrite negbK -(Lagrange_index sKL sCK) natrM => lb_KA.
pose S2 : seq 'CF(L) := [::]; pose S1 := S2 ++ S A; rewrite -[S A]/S1 in cohA.
have ccsS1S: cfConjC_subset S1 calS by apply: seqInd_conjC_subset1.
@@ -153,7 +153,7 @@ have sAbZH: (A / B \subset 'Z(H / B))%g.
by apply: homg_quotientS; rewrite ?(subset_trans sHL) ?normal_norm.
have ltAH: A \proper H.
by rewrite properEneq sAH (contraTneq _ lbHA) // => ->; rewrite indexgg addn1.
-set x := sqrtC #|H : A|%:R.
+set x : algC := sqrtC #|H : A|%:R.
have [nz_x x_gt0]: x != 0 /\ 0 < x by rewrite gtr_eqF sqrtC_gt0 gt0CiG.
without loss{cohA} ubKA: / #|K : A|%:R - 1 <= 2%:R * #|L : H|%:R * x.
have [sAK ltAK] := (subset_trans sAH sHK, proper_sub_trans ltAH sHK).
diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v
index cea9319..4610829 100644
--- a/mathcomp/odd_order/PFsection7.v
+++ b/mathcomp/odd_order/PFsection7.v
@@ -324,7 +324,7 @@ transitivity (\sum_(x in A) \sum_(xi <- S) \sum_(mu <- S) F xi mu x).
apply: eq_bigr => x Ax; rewrite part_a // sum_cfunE -mulrA mulr_suml.
apply: eq_bigr => xi _; rewrite mulrA -mulr_suml rmorph_sum; congr (_ * _).
rewrite mulr_sumr; apply: eq_bigr => mu _; rewrite !cfunE (cfdotC mu).
- rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -4!mulrA 2!(mulrCA _^-1).
+ rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -3!mulrA 2!(mulrCA _^-1).
by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) mulrA 2!(mulrA _^*).
rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=.
apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:21:40 +0000