Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21611 #77

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 1 commit into from
Feb 18, 2026
Merged

Adapt to https://github.com/rocq-prover/rocq/pull/21611 #77

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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/BGsection7.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ Reserved Notation "|/|* ( A ; pi )" (format "|/|* ( A ; pi )").

(* The generic setup for the whole Odd Order Theorem proof. *)

HB.mixin Record IsMinSimpleOddGroup gT of FinGroup gT := {
HB.mixin Record IsMinSimpleOddGroup gT & FinGroup gT := {
mFT_odd_full : odd #|[set: gT]|;
mFT_simple : simple [set: gT];
mFT_nonSolvable : ~~ solvable [set: gT];
Expand Down
2 changes: 1 addition & 1 deletion theories/PFsection2.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ Qed.

Fact Dade_signalizer_key : unit. Proof. by []. Qed.
Definition Dade_signalizer_def a := 'O_pi^'('C_G[a])%G.
Definition Dade_signalizer of Dade_hypothesis G L A :=
Definition Dade_signalizer & Dade_hypothesis G L A :=
locked_with Dade_signalizer_key Dade_signalizer_def.

Hypothesis ddA : Dade_hypothesis G L A.
Expand Down
2 changes: 1 addition & 1 deletion theories/PFsection3.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ Section Definitions.

Variables (gT : finGroupType) (G W W1 W2 : {set gT}).

Definition cyclicTIset of W1 \x W2 = W := W :\: (W1 :|: W2).
Definition cyclicTIset & W1 \x W2 = W := W :\: (W1 :|: W2).

Definition cyclicTI_hypothesis (defW : W1 \x W2 = W) :=
[/\ cyclic W, odd #|W| & normedTI (cyclicTIset defW) G W].
Expand Down
2 changes: 1 addition & 1 deletion theories/PFsection4.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ by case/and3P=> _ _ /andP[] /andP[] /eqP.
Qed.

(* This is Peterfalvi, Hypothesis (4.2), with explicit parameters. *)
Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) of W1 \x W2 = W :=
Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) & W1 \x W2 = W :=
[/\ (*a*) [/\ K ><| W1 = L, W1 != 1, Hall L W1 & cyclic W1],
(*b*) [/\ W2 != 1, W2 \subset K & cyclic W2],
{in W1^#, forall x, 'C_K[x] = W2}
Expand Down
2 changes: 1 addition & 1 deletion theories/PFsection9.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ by rewrite -(@leq_pmul2l (p ^ q)) -?oH ?cUW2 //= expn_gt0 cardG_gt0.
Qed.

(* Existential witnesses for Peterfalvi (9.4). *)
Definition Ptype_Fcore_kernel of of_typeP M U defW :=
Definition Ptype_Fcore_kernel & of_typeP M U defW :=
odflt 1%G [pick H0 : {group gT} | chief_factor M H0 H & 'C_H(U) \subset H0].
Let H0 := (Ptype_Fcore_kernel MtypeP).
Local Notation "` 'H0'" := (gval H0) (only parsing) : group_scope.
Expand Down