Skip to content

Adapt to math-comp/math-comp#1404 #75

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 2 commits into from
Sep 24, 2025
Merged

Adapt to math-comp/math-comp#1404 #75

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d7c0efe
Adapt to math-comp/math-comp#1404
pi8027 Sep 18, 2025
d12b42e
adapt to the removal of the conjC notation from classfun.v
affeldt-aist Sep 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion theories/PFsection10.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ have cohS2 : coherent_with S2 M^# tau tau1 := subset_coherent_with sS21 cohS1.
have irrS2: {subset S2 <= irr M} by apply/allP; rewrite /= cfAut_irr irr_zeta.
rewrite (FTtype345_bridge_coherence cohS2 Dalpha) //; last first.
rewrite -[X]opprK cfdotNr opprD cfdotDr nY_n2 cfdotNl cfdotNr opprK cfdotZl.
by rewrite cfdotC alpha_zeta_n rmorphN conj_natr // mulrN addNr oppr0.
by rewrite cfdotC alpha_zeta_n rmorphN/= conj_natr // mulrN addNr oppr0.
split=> [|_ /sS21/sS10//|]; last first.
by apply/allP; rewrite /= !inE cfConjCK !eqxx orbT.
by rewrite /= inE eq_sym; have [[_ /hasPn-> //]] := scohS0; apply: sS10.
Expand Down
4 changes: 2 additions & 2 deletions theories/PFsection11.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory.
Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory Num.Def.

Section Eleven.

Expand Down Expand Up @@ -867,7 +867,7 @@ have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1.
rewrite cfdotC Dphi cfdotDl (orthoPl oXS1) ?map_f // addr0.
rewrite defY cfdotBl scaler_sumr cfproj_sum_orthonormal //.
rewrite cfdotZl Itau1 ?mem_zchar ?n1S1 // mulr1 rmorphB opprD opprK.
by rewrite Dn rmorph_nat conj_intr.
by rewrite Dn rmorph_nat/= conj_intr.
have a_even: (2 %| a)%C. (* Third internal part of (11.8.5). *)
have Zbeta: beta \in 'Z[irr G].
rewrite -{1}(betaE i j) // rpredD ?rpredB ?Zphi ?cycTIiso_vchar //.
Expand Down
4 changes: 1 addition & 3 deletions theories/PFsection14.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory.
Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory Num.Def.

Section Fourteen.

Expand Down Expand Up @@ -1257,5 +1257,3 @@ Proof. exact: (minSimpleOdd_ind no_minSimple_odd_group). Qed.
Theorem simple_odd_group_prime (gT : finGroupType) (G : {group gT}) :
odd #|G| -> simple G -> prime #|G|.
Proof. exact: (minSimpleOdd_prime no_minSimple_odd_group). Qed.


2 changes: 1 addition & 1 deletion theories/PFsection5.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope Order.TTheory GRing.Theory Num.Theory.
Import GroupScope Order.TTheory GRing.Theory Num.Theory Num.Def.
Local Open Scope ring_scope.

(* Results about the set of induced irreducible characters *)
Expand Down
10 changes: 5 additions & 5 deletions theories/PFsection9.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope Order.TTheory GRing.Theory FinRing.Theory.
Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory Num.Def.

Section Nine.

Expand Down Expand Up @@ -2121,7 +2121,7 @@ have [Gamma [S4_Gamma normGamma [b Dbeta]]]:
rewrite -raddfB Dtau1 // Itau //; last first.
by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi).
rewrite cfdotC cfdotBr cfdotZr !cfdotBl 2?oSS ?(memPn S1'lam1) // subrr.
by rewrite add0r n1psi1 oSS // subr0 mulr1 rmorphN conjCK subrr scale0r.
by rewrite add0r n1psi1 oSS // subr0 mulr1 rmorphN/= conjCK subrr scale0r.
have Gge1: 1 <= '[G] ?= iff ('[G] == 1).
rewrite eq_sym; apply: leif_eq.
have N_G: '[G] \in Num.nat.
Expand All @@ -2147,9 +2147,9 @@ have [Gamma [S4_Gamma normGamma [b Dbeta]]]:
congr (_ + _); rewrite dB scaleNr [- _ + _]addrC cfnormB !cfnormZ.
rewrite normr_nat intr_normK // scaler_sumr cfdotZr rmorph_nat.
rewrite cfnorm_map_orthonormal // cfproj_sum_orthonormal //.
rewrite Itau1 ?mem_zchar// n1psi1 mulr1 rmorphM/= rmorph_nat conj_intr //.
rewrite -mulr2n oS1ua -muln_divA // mul2n -addrA addrCA -natrX mulrBl.
by congr (_ + (_ - _)); rewrite -mulrnAl -mulrnA muln2 mulrC.
rewrite Itau1 ?mem_zchar// n1psi1 mulr1 [conjC _]rmorphM/= rmorph_nat.
rewrite conj_intr // -mulr2n oS1ua -muln_divA // -addrA addrCA mulrBl.
by rewrite -mulrnAl -mulrnA mul2n muln2 -natrX [b * _]mulrC.
rewrite Itau // cfnormBd; last first.
by rewrite cfdotZr oSS ?mulr0 // (memPnC S1'lam1).
by rewrite cfnormZ normr_nat n1psi1 n1lam1 mulr1 addrC -natrX.
Expand Down
Loading