From d26c8879b048141d98d61918edcf2f82fa47cff4 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Tue, 3 Dec 2024 16:24:39 +0100 Subject: [PATCH] Commented out unneded argument specif + presentation_S5 (very long to Qed) --- theories/MPoly/homogsym.v | 4 ++-- theories/MPoly/sympoly.v | 2 +- theories/SymGroup/presentSn.v | 2 ++ 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/theories/MPoly/homogsym.v b/theories/MPoly/homogsym.v index 08be98f..87652da 100644 --- a/theories/MPoly/homogsym.v +++ b/theories/MPoly/homogsym.v @@ -145,8 +145,8 @@ End DefType. (* We need to break off the section here to let the argument scope *) (* directives take effect. *) Bind Scope ring_scope with homogsym. -Arguments homogsym n%_N R%_R. -Arguments homsym_inj n%_N R%_R d%_N. +(* Arguments homogsym n%_N R%_R. *) +(* Arguments homsym_inj n%_N R%_R d%_N. *) Notation "{ 'homsym' T [ n , d ] }" := (homogsym n T d). diff --git a/theories/MPoly/sympoly.v b/theories/MPoly/sympoly.v index fce9e58..7100edb 100644 --- a/theories/MPoly/sympoly.v +++ b/theories/MPoly/sympoly.v @@ -158,7 +158,7 @@ End DefType. (* We need to break off the section here to let the argument scope *) (* directives take effect. *) Bind Scope ring_scope with sympoly. -Arguments sympol n%_N R%_R. +(* Arguments sympol {n}%nat_scope {R}%ring_scope. *) Notation "{ 'sympoly' T [ n ] }" := (sympoly n T). diff --git a/theories/SymGroup/presentSn.v b/theories/SymGroup/presentSn.v index 82ff32c..cccbd38 100644 --- a/theories/SymGroup/presentSn.v +++ b/theories/SymGroup/presentSn.v @@ -2295,6 +2295,7 @@ apply intro_isoGrp. by apply/imsetP => /=; exists (inord 2); rewrite //= inordK. Qed. +(* too long to QED Lemma presentation_S5 : 'SG_5 \isog Grp ( s0 : s1 : s2 : s3 : @@ -2341,3 +2342,4 @@ apply intro_isoGrp. + exists 's_3; rewrite ?setTI ?Hf //. by apply/imsetP => /=; exists (inord 3); rewrite //= inordK. Qed. +*)