From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.fingroup.presentation.html | 95 ++++++++++++------------ 1 file changed, 47 insertions(+), 48 deletions(-) (limited to 'docs/htmldoc/mathcomp.fingroup.presentation.html') diff --git a/docs/htmldoc/mathcomp.fingroup.presentation.html b/docs/htmldoc/mathcomp.fingroup.presentation.html index 319155d..301b4f4 100644 --- a/docs/htmldoc/mathcomp.fingroup.presentation.html +++ b/docs/htmldoc/mathcomp.fingroup.presentation.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -110,10 +109,10 @@
Inductive term :=
-  | Cst of nat
+  | Cst of nat
  | Idx
  | Inv of term
-  | Exp of term & nat
+  | Exp of term & nat
  | Mul of term & term
  | Conj of term & term
  | Comm of term & term.
@@ -123,11 +122,11 @@   match t with
  | Cst i ⇒ nth 1 e i
  | Idx ⇒ 1
-  | Inv t1 ⇒ (eval e t1)^-1
-  | Exp t1 n ⇒ eval e t1 ^+ n
-  | Mul t1 t2 ⇒ eval e t1 × eval e t2
-  | Conj t1 t2 ⇒ eval e t1 ^ eval e t2
-  | Comm t1 t2 ⇒ [~ eval e t1, eval e t2]
+  | Inv t1 ⇒ (eval e t1)^-1
+  | Exp t1 n ⇒ eval e t1 ^+ n
+  | Mul t1 t2 ⇒ eval e t1 × eval e t2
+  | Conj t1 t2 ⇒ eval e t1 ^ eval e t2
+  | Comm t1 t2 ⇒ [~ eval e t1, eval e t2]
  end.

@@ -139,11 +138,11 @@ Inductive rel_type := NoRel | Rel vT of vT & vT.

-Definition bool_of_rel r := if r is Rel vT v1 v2 then v1 == v2 else true.
+Definition bool_of_rel r := if r is Rel vT v1 v2 then v1 == v2 else true.

Definition and_rel vT (v1 v2 : vT) r :=
-  if r is Rel wT w1 w2 then Rel (v1, w1) (v2, w2) else Rel v1 v2.
+  if r is Rel wT w1 w2 then Rel (v1, w1) (v2, w2) else Rel v1 v2.

Fixpoint rel {gT} (e : seq gT) f r :=
@@ -153,27 +152,27 @@   end.

-Inductive type := Generator of term → type | Formula of formula.
+Inductive type := Generator of term → type | Formula of formula.
Definition Cast p : type := p. (* syntactic scope cast *)

-Inductive env gT := Env of {set gT} & seq gT.
-Definition env1 {gT} (x : gT : finType) := Env <[x]> [:: x].
+Inductive env gT := Env of {set gT} & seq gT.
+Definition env1 {gT} (x : gT : finType) := Env <[x]> [:: x].

-Fixpoint sat gT vT B n (s : vT → env gT) p :=
+Fixpoint sat gT vT B n (s : vT → env gT) p :=
  match p with
  | Formula f ⇒
-    [∃ v, let: Env A e := s v in and_rel A B (rel (rev e) f NoRel)]
+    [∃ v, let: Env A e := s v in and_rel A B (rel (rev e) f NoRel)]
  | Generator p' ⇒
-    let s' v := let: Env A e := s v.1 in Env (A <*> <[v.2]>) (v.2 :: e) in
-    sat B n.+1 s' (p' (Cst n))
+    let s' v := let: Env A e := s v.1 in Env (A <*> <[v.2]>) (v.2 :: e) in
+    sat B n.+1 s' (p' (Cst n))
  end.

-Definition hom gT (B : {set gT}) p := sat B 1 env1 (p (Cst 0)).
-Definition iso gT (B : {set gT}) p :=
-  ∀ rT (H : {group rT}), (H \homg B) = hom H p.
+Definition hom gT (B : {set gT}) p := sat B 1 env1 (p (Cst 0)).
+Definition iso gT (B : {set gT}) p :=
+  ∀ rT (H : {group rT}), (H \homg B) = hom H p.

End Presentation.
@@ -196,19 +195,19 @@ Declare (implicitly) the argument scope tags.
-Notation "1" := Idx : group_presentation.
+Notation "1" := Idx : group_presentation.

-Infix "×" := Mul : group_presentation.
-Infix "^+" := Exp : group_presentation.
-Infix "^" := Conj : group_presentation.
-Notation "x ^-1" := (Inv x) : group_presentation.
-Notation "x ^- n" := (Inv (x ^+ n)) : group_presentation.
-Notation "[ ~ x1 , x2 , .. , xn ]" :=
+Infix "×" := Mul : group_presentation.
+Infix "^+" := Exp : group_presentation.
+Infix "^" := Conj : group_presentation.
+Notation "x ^-1" := (Inv x) : group_presentation.
+Notation "x ^- n" := (Inv (x ^+ n)) : group_presentation.
+Notation "[ ~ x1 , x2 , .. , xn ]" :=
  (Comm .. (Comm x1 x2) .. xn) : group_presentation.
-Notation "x = y" := (Eq2 x y) : group_presentation.
-Notation "x = y = z" := (Eq3 x y z) : group_presentation.
-Notation "( r1 , r2 , .. , rn )" :=
+Notation "x = y" := (Eq2 x y) : group_presentation.
+Notation "x = y = z" := (Eq3 x y z) : group_presentation.
+Notation "( r1 , r2 , .. , rn )" :=
  (And .. (And r1 r2) .. rn) : group_presentation.

@@ -218,26 +217,26 @@ Declare (implicitly) the argument scope tags.
-Notation "x : p" := (fun x ⇒ Cast p) : nt_group_presentation.
+Notation "x : p" := (fun x ⇒ Cast p) : nt_group_presentation.

-Notation "x : p" := (Generator (x : p)) : group_presentation.
+Notation "x : p" := (Generator (x : p)) : group_presentation.

-Notation "H \homg 'Grp' p" := (hom H p)
+Notation "H \homg 'Grp' p" := (hom H p)
  (at level 70, p at level 0, format "H \homg 'Grp' p") : group_scope.

-Notation "H \isog 'Grp' p" := (iso H p)
+Notation "H \isog 'Grp' p" := (iso H p)
  (at level 70, p at level 0, format "H \isog 'Grp' p") : group_scope.

-Notation "H \homg 'Grp' ( x : p )" := (hom H (x : p))
+Notation "H \homg 'Grp' ( x : p )" := (hom H (x : p))
  (at level 70, x at level 0,
   format "'[hv' H '/ ' \homg 'Grp' ( x : p ) ']'") : group_scope.

-Notation "H \isog 'Grp' ( x : p )" := (iso H (x : p))
+Notation "H \isog 'Grp' ( x : p )" := (iso H (x : p))
  (at level 70, x at level 0,
   format "'[hv' H '/ ' \isog 'Grp' ( x : p ) ']'") : group_scope.
@@ -251,28 +250,28 @@ Import Presentation.

-Lemma isoGrp_hom gT (G : {group gT}) p : G \isog Grp p → G \homg Grp p.
+Lemma isoGrp_hom gT (G : {group gT}) p : G \isog Grp p → G \homg Grp p.

-Lemma isoGrpP gT (G : {group gT}) p rT (H : {group rT}) :
-  G \isog Grp p → reflect (#|H| = #|G| ∧ H \homg Grp p) (H \isog G).
+Lemma isoGrpP gT (G : {group gT}) p rT (H : {group rT}) :
+  G \isog Grp p → reflect (#|H| = #|G| ∧ H \homg Grp p) (H \isog G).

-Lemma homGrp_trans rT gT (H : {set rT}) (G : {group gT}) p :
-  H \homg G → G \homg Grp p → H \homg Grp p.
+Lemma homGrp_trans rT gT (H : {set rT}) (G : {group gT}) p :
+  H \homg G → G \homg Grp p → H \homg Grp p.

-Lemma eq_homGrp gT rT (G : {group gT}) (H : {group rT}) p :
-  G \isog H → (G \homg Grp p) = (H \homg Grp p).
+Lemma eq_homGrp gT rT (G : {group gT}) (H : {group rT}) p :
+  G \isog H → (G \homg Grp p) = (H \homg Grp p).

-Lemma isoGrp_trans gT rT (G : {group gT}) (H : {group rT}) p :
-  G \isog H → H \isog Grp p → G \isog Grp p.
+Lemma isoGrp_trans gT rT (G : {group gT}) (H : {group rT}) p :
+  G \isog H → H \isog Grp p → G \isog Grp p.

-Lemma intro_isoGrp gT (G : {group gT}) p :
-    G \homg Grp p → (∀ rT (H : {group rT}), H \homg Grp p → H \homg G) →
-  G \isog Grp p.
+Lemma intro_isoGrp gT (G : {group gT}) p :
+    G \homg Grp p → (∀ rT (H : {group rT}), H \homg Grp p → H \homg G) →
+  G \isog Grp p.

End PresentationTheory.
-- cgit v1.2.3