Commented out unneded argument specif + presentation_S5 (very long to…

… Qed)
math-comp · Dec 3, 2024 · d26c887 · d26c887
1 parent 05b1bd6
commit d26c887
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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.
+*)