From d7c0efe4764e95e82462c0b5138bb3688b3b3adb Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 18 Sep 2025 19:31:06 +0200 Subject: [PATCH 1/2] Adapt to math-comp/math-comp#1404 --- theories/PFsection10.v | 2 +- theories/PFsection11.v | 2 +- theories/PFsection9.v | 8 ++++---- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/PFsection10.v b/theories/PFsection10.v index 282ad69..6cf052d 100644 --- a/theories/PFsection10.v +++ b/theories/PFsection10.v @@ -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. diff --git a/theories/PFsection11.v b/theories/PFsection11.v index 681d984..589ec94 100644 --- a/theories/PFsection11.v +++ b/theories/PFsection11.v @@ -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 //. diff --git a/theories/PFsection9.v b/theories/PFsection9.v index 78a7187..f02006b 100644 --- a/theories/PFsection9.v +++ b/theories/PFsection9.v @@ -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. @@ -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. From d12b42e0396d84fb64dc0f08b0e61616e3871335 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 24 Sep 2025 15:05:50 +0900 Subject: [PATCH 2/2] adapt to the removal of the conjC notation from classfun.v --- theories/PFsection11.v | 2 +- theories/PFsection14.v | 4 +--- theories/PFsection5.v | 2 +- theories/PFsection9.v | 2 +- 4 files changed, 4 insertions(+), 6 deletions(-) diff --git a/theories/PFsection11.v b/theories/PFsection11.v index 589ec94..94536ca 100644 --- a/theories/PFsection11.v +++ b/theories/PFsection11.v @@ -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. diff --git a/theories/PFsection14.v b/theories/PFsection14.v index 0df9f1d..71f84de 100644 --- a/theories/PFsection14.v +++ b/theories/PFsection14.v @@ -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. @@ -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. - - diff --git a/theories/PFsection5.v b/theories/PFsection5.v index baf5627..8a17fe4 100644 --- a/theories/PFsection5.v +++ b/theories/PFsection5.v @@ -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 *) diff --git a/theories/PFsection9.v b/theories/PFsection9.v index f02006b..4597e46 100644 --- a/theories/PFsection9.v +++ b/theories/PFsection9.v @@ -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.