| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (259 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (96 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (66 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
A
absZ [definition, in GroupTheory.Z.Zbase]abs_eq_or_oppZ [lemma, in GroupTheory.Z.Zadd]
addZ [definition, in GroupTheory.Z.Zadd]
addZ_neutral [lemma, in GroupTheory.Z.Zadd]
addZ_associativity [lemma, in GroupTheory.Z.Zadd]
addZ_commutativity [lemma, in GroupTheory.Z.Zadd]
addZ_eq5 [lemma, in GroupTheory.Z.Zadd]
addZ_eq4 [lemma, in GroupTheory.Z.Zadd]
addZ_eq3 [lemma, in GroupTheory.Z.Zadd]
addZ_eq2 [lemma, in GroupTheory.Z.Zadd]
addZ_eq1 [lemma, in GroupTheory.Z.Zadd]
add_exponents [lemma, in GroupTheory.g1]
add_mIZ_predZ [lemma, in GroupTheory.Z.Zadd]
add_IZ_succZ [lemma, in GroupTheory.Z.Zadd]
add_OZ [lemma, in GroupTheory.Z.Zadd]
add1 [definition, in GroupTheory.Z.Zadd]
add2 [definition, in GroupTheory.Z.Zadd]
Antisymmetric [definition, in GroupTheory.Relations]
associative [definition, in GroupTheory.Z.Zadd]
associative [definition, in GroupTheory.Laws]
auxsub [lemma, in GroupTheory.g2]
B
Basic_laws.D [variable, in GroupTheory.Laws]Basic_laws.op [variable, in GroupTheory.Laws]
Basic_laws.U [variable, in GroupTheory.Laws]
Basic_laws [section, in GroupTheory.Laws]
C
cancellation [lemma, in GroupTheory.gr]cancellation' [definition, in GroupTheory.g1]
change_exponent_sign [lemma, in GroupTheory.g1]
Cinq [section, in GroupTheory.g3]
Cinq.h [variable, in GroupTheory.g3]
Cinq.H [variable, in GroupTheory.g3]
Cinq.H_Finite [variable, in GroupTheory.g3]
Cinq.H_included_in_G [variable, in GroupTheory.g3]
Cinq.H_inhabited [variable, in GroupTheory.g3]
Cinq.stability [variable, in GroupTheory.g3]
commutative [definition, in GroupTheory.Z.Zadd]
commutative [definition, in GroupTheory.Laws]
D
Definition_of_Prod [constructor, in GroupTheory.g2]Definition_of_subgroup [constructor, in GroupTheory.Group_definitions]
E
e [definition, in GroupTheory.g1]eh_is_e [lemma, in GroupTheory.g1]
eH_in_G [lemma, in GroupTheory.g1]
Elements [section, in GroupTheory.g1]
Elements.H [variable, in GroupTheory.g1]
Elements.sub [variable, in GroupTheory.g1]
endo_operation [definition, in GroupTheory.Laws]
endo_function [definition, in GroupTheory.Laws]
Equivalence [definition, in GroupTheory.Relations]
Equiv_from_order [lemma, in GroupTheory.Relations]
eq_gt_O_dec [lemma, in GroupTheory.Z.Nat_complements]
eq_OZ_dec [lemma, in GroupTheory.Z.Zbase]
exp [definition, in GroupTheory.g1]
exp_commut1 [lemma, in GroupTheory.g1]
exp_l2' [lemma, in GroupTheory.g1]
exp_l2 [lemma, in GroupTheory.g1]
exp_l1 [lemma, in GroupTheory.g1]
exp_unfold_neg [lemma, in GroupTheory.g1]
exp_unfold_pos [lemma, in GroupTheory.g1]
exp_endo [lemma, in GroupTheory.g1]
Ex1 [lemma, in GroupTheory.g1]
Ex2 [lemma, in GroupTheory.g1]
Ex3 [lemma, in GroupTheory.g1]
Ex4 [lemma, in GroupTheory.g1]
Ex5 [lemma, in GroupTheory.g1]
e_ [projection, in GroupTheory.Group_definitions]
G
G [definition, in GroupTheory.g1]Gr [axiom, in GroupTheory.g1]
gr [library]
Group [record, in GroupTheory.Group_definitions]
group [constructor, in GroupTheory.Group_definitions]
group_trivialities.e [variable, in GroupTheory.gr]
group_trivialities.inv [variable, in GroupTheory.gr]
group_trivialities.star [variable, in GroupTheory.gr]
group_trivialities.G [variable, in GroupTheory.gr]
group_trivialities.Gr [variable, in GroupTheory.gr]
group_trivialities.U [variable, in GroupTheory.gr]
group_trivialities [section, in GroupTheory.gr]
group_definition.U [variable, in GroupTheory.Group_definitions]
group_definition [section, in GroupTheory.Group_definitions]
Group_definitions [library]
G_ [projection, in GroupTheory.Group_definitions]
G0 [definition, in GroupTheory.gr]
G0_ [projection, in GroupTheory.Group_definitions]
G0' [definition, in GroupTheory.g1]
G1 [definition, in GroupTheory.gr]
g1 [library]
G1_ [projection, in GroupTheory.Group_definitions]
G1' [definition, in GroupTheory.g1]
g2 [library]
G2a [definition, in GroupTheory.gr]
G2a_ [projection, in GroupTheory.Group_definitions]
G2a' [definition, in GroupTheory.g1]
G2b [definition, in GroupTheory.gr]
G2b_ [projection, in GroupTheory.Group_definitions]
G2b' [definition, in GroupTheory.g1]
G2c [definition, in GroupTheory.gr]
G2c_ [projection, in GroupTheory.Group_definitions]
G2c' [definition, in GroupTheory.g1]
g3 [library]
G3a [definition, in GroupTheory.gr]
G3a_ [projection, in GroupTheory.Group_definitions]
G3a' [definition, in GroupTheory.g1]
G3b [definition, in GroupTheory.gr]
G3b_ [projection, in GroupTheory.Group_definitions]
G3b' [definition, in GroupTheory.g1]
G3c [definition, in GroupTheory.gr]
G3c_ [projection, in GroupTheory.Group_definitions]
G3c' [definition, in GroupTheory.g1]
I
IdZ [definition, in GroupTheory.Z.Zadd]inv [definition, in GroupTheory.g1]
invH_is_inv [lemma, in GroupTheory.g1]
inv_endo [lemma, in GroupTheory.g1]
inv_involution' [definition, in GroupTheory.g1]
inv_star' [definition, in GroupTheory.g1]
inv_involution [lemma, in GroupTheory.gr]
inv_star [lemma, in GroupTheory.gr]
inv_ [projection, in GroupTheory.Group_definitions]
In_powers [constructor, in GroupTheory.g1]
is_posn [definition, in GroupTheory.Z.Zbase]
IZ [definition, in GroupTheory.Z.Zbase]
L
Laws [library]left_inverse [definition, in GroupTheory.Laws]
left_neutral [definition, in GroupTheory.Laws]
leZ [definition, in GroupTheory.Z.Zle]
leZ_antisymmetric [lemma, in GroupTheory.Z.Zle]
le_opp_OZ2 [lemma, in GroupTheory.Z.Zle]
le_opp_OZ [lemma, in GroupTheory.Z.Zle]
le_opp_OZ_l [lemma, in GroupTheory.Z.Zle]
ltZ [definition, in GroupTheory.Z.Zle]
lt_absZ [definition, in GroupTheory.Z.Zle]
lt_succ [lemma, in GroupTheory.Z.Nat_complements]
lt_minus2 [lemma, in GroupTheory.Z.Nat_complements]
l1 [lemma, in GroupTheory.g1]
M
minus_n_Sm [lemma, in GroupTheory.Z.Nat_complements]N
Nat_complements [library]neg [constructor, in GroupTheory.Z.Zbase]
negOZ [definition, in GroupTheory.Z.Zbase]
neutral [definition, in GroupTheory.Z.Zadd]
O
oppZ [definition, in GroupTheory.Z.Zadd]opp_inv [variable, in GroupTheory.Z.Zle]
opp_predZ [lemma, in GroupTheory.Z.Zadd]
opp_succZ [lemma, in GroupTheory.Z.Zadd]
Order [definition, in GroupTheory.Relations]
OZ [constructor, in GroupTheory.Z.Zbase]
P
PER [definition, in GroupTheory.Relations]phi [definition, in GroupTheory.g3]
phi_exp [lemma, in GroupTheory.g3]
phi_unfold [lemma, in GroupTheory.g3]
pos [constructor, in GroupTheory.Z.Zbase]
positive_powers [lemma, in GroupTheory.g3]
posOZ [definition, in GroupTheory.Z.Zbase]
powers [inductive, in GroupTheory.g1]
powers_of_one_element [lemma, in GroupTheory.g1]
powers_repeat [lemma, in GroupTheory.g3]
predZ [definition, in GroupTheory.Z.Z_succ_pred]
pred_succZ [lemma, in GroupTheory.Z.Z_succ_pred]
pred_addZ_r [lemma, in GroupTheory.Z.Zadd]
pred_addZ_l [lemma, in GroupTheory.Z.Zadd]
Premier [section, in GroupTheory.g1]
Premier.assoc [variable, in GroupTheory.g1]
Premier.eH [variable, in GroupTheory.g1]
Premier.eH_right_neutral [variable, in GroupTheory.g1]
Premier.eH_left_neutral [variable, in GroupTheory.g1]
Premier.eH_in_H [variable, in GroupTheory.g1]
Premier.GrH [variable, in GroupTheory.g1]
Premier.H [variable, in GroupTheory.g1]
Premier.hinv [variable, in GroupTheory.g1]
Premier.hstar [variable, in GroupTheory.g1]
Premier.inhabited [variable, in GroupTheory.g1]
Premier.inv_right_inverse [variable, in GroupTheory.g1]
Premier.inv_left_inverse [variable, in GroupTheory.g1]
Premier.subset [variable, in GroupTheory.g1]
Premier.witness [variable, in GroupTheory.g1]
Prod [inductive, in GroupTheory.g2]
psi [definition, in GroupTheory.g3]
psi_not_inj [lemma, in GroupTheory.g3]
Q
Quatre [section, in GroupTheory.g2]Quatre.H [variable, in GroupTheory.g2]
Quatre.K [variable, in GroupTheory.g2]
Quatre.subH [variable, in GroupTheory.g2]
Quatre.subK [variable, in GroupTheory.g2]
R
Reflexive [definition, in GroupTheory.Relations]Relation [definition, in GroupTheory.Relations]
Relations [section, in GroupTheory.Relations]
Relations [library]
Relations.R [variable, in GroupTheory.Relations]
Relations.U [variable, in GroupTheory.Relations]
remaining [lemma, in GroupTheory.g3]
resolve [lemma, in GroupTheory.gr]
resolve' [definition, in GroupTheory.g1]
right_inverse [definition, in GroupTheory.Laws]
right_neutral [definition, in GroupTheory.Laws]
S
Second [section, in GroupTheory.g1]Second.eH [variable, in GroupTheory.g1]
Second.H [variable, in GroupTheory.g1]
Second.h0 [variable, in GroupTheory.g1]
Second.h1 [variable, in GroupTheory.g1]
Second.h2 [variable, in GroupTheory.g1]
Second.witness [variable, in GroupTheory.g1]
self_inv' [definition, in GroupTheory.g1]
self_inv [lemma, in GroupTheory.gr]
Setsubgroup [definition, in GroupTheory.Group_definitions]
sgnZ [definition, in GroupTheory.Z.Zbase]
sign_absZ [lemma, in GroupTheory.Z.Zle]
star [definition, in GroupTheory.g1]
starH_is_star [lemma, in GroupTheory.g1]
star_endo [lemma, in GroupTheory.g1]
star_ [projection, in GroupTheory.Group_definitions]
subgroup [inductive, in GroupTheory.Group_definitions]
Subgroup_inhabited [lemma, in GroupTheory.g1]
succZ [definition, in GroupTheory.Z.Z_succ_pred]
succ_pred_pred_succZ [lemma, in GroupTheory.Z.Z_succ_pred]
succ_predZ [lemma, in GroupTheory.Z.Z_succ_pred]
succ_addZ_r [lemma, in GroupTheory.Z.Zadd]
succ_addZ_l [lemma, in GroupTheory.Z.Zadd]
Symmetric [definition, in GroupTheory.Relations]
sym_not_P [lemma, in GroupTheory.Relations]
T
technical_lemma [lemma, in GroupTheory.Z.Nat_complements]tech_opp_pos_negZ2 [lemma, in GroupTheory.g1]
tech_opp_pos_negZ1 [lemma, in GroupTheory.g1]
tech_posOZ_pos [lemma, in GroupTheory.Z.Zle]
tech_lt_abs_OZ [lemma, in GroupTheory.Z.Zle]
tech_le_pos_abs [lemma, in GroupTheory.Z.Zle]
tech_succ_posOZ [lemma, in GroupTheory.Z.Z_succ_pred]
tech_pred_posZ [lemma, in GroupTheory.Z.Z_succ_pred]
tech_pos_not_posZ [lemma, in GroupTheory.Z.Zbase]
tech_opp_pos_negZ [lemma, in GroupTheory.Z.Zadd]
tech_add_neg_negZ [lemma, in GroupTheory.Z.Zadd]
tech_add_pos_posZ [lemma, in GroupTheory.Z.Zadd]
tech_add_neg_posZ [lemma, in GroupTheory.Z.Zadd]
tech_add_pos_negZ [lemma, in GroupTheory.Z.Zadd]
tech_add_pos_neg_posZ [lemma, in GroupTheory.Z.Zadd]
tech_add_neg_predZ [lemma, in GroupTheory.Z.Zadd]
tech_add_pos_succZ [lemma, in GroupTheory.Z.Zadd]
tech_exp' [lemma, in GroupTheory.g3]
tech_exp [lemma, in GroupTheory.g3]
Transitive [definition, in GroupTheory.Relations]
triv1 [lemma, in GroupTheory.gr]
triv1' [definition, in GroupTheory.g1]
triv2 [lemma, in GroupTheory.gr]
triv2' [definition, in GroupTheory.g1]
Trois [section, in GroupTheory.g2]
Trois.H [variable, in GroupTheory.g2]
Trois.K [variable, in GroupTheory.g2]
Trois.subH [variable, in GroupTheory.g2]
Trois.subK [variable, in GroupTheory.g2]
T_1_6_3 [lemma, in GroupTheory.g1]
T_1_6_2 [lemma, in GroupTheory.g1]
T_1_6_8 [lemma, in GroupTheory.g2]
T_1_6_4 [lemma, in GroupTheory.g3]
T4 [lemma, in GroupTheory.g2]
T4R [lemma, in GroupTheory.g2]
T4R1 [lemma, in GroupTheory.g2]
U
U [axiom, in GroupTheory.g1]Z
Z [inductive, in GroupTheory.Z.Zbase]Zadd [library]
Zbase [library]
Zle [library]
Z_succ_pred [library]
Variable Index
B
Basic_laws.D [in GroupTheory.Laws]Basic_laws.op [in GroupTheory.Laws]
Basic_laws.U [in GroupTheory.Laws]
C
Cinq.h [in GroupTheory.g3]Cinq.H [in GroupTheory.g3]
Cinq.H_Finite [in GroupTheory.g3]
Cinq.H_included_in_G [in GroupTheory.g3]
Cinq.H_inhabited [in GroupTheory.g3]
Cinq.stability [in GroupTheory.g3]
E
Elements.H [in GroupTheory.g1]Elements.sub [in GroupTheory.g1]
G
group_trivialities.e [in GroupTheory.gr]group_trivialities.inv [in GroupTheory.gr]
group_trivialities.star [in GroupTheory.gr]
group_trivialities.G [in GroupTheory.gr]
group_trivialities.Gr [in GroupTheory.gr]
group_trivialities.U [in GroupTheory.gr]
group_definition.U [in GroupTheory.Group_definitions]
O
opp_inv [in GroupTheory.Z.Zle]P
Premier.assoc [in GroupTheory.g1]Premier.eH [in GroupTheory.g1]
Premier.eH_right_neutral [in GroupTheory.g1]
Premier.eH_left_neutral [in GroupTheory.g1]
Premier.eH_in_H [in GroupTheory.g1]
Premier.GrH [in GroupTheory.g1]
Premier.H [in GroupTheory.g1]
Premier.hinv [in GroupTheory.g1]
Premier.hstar [in GroupTheory.g1]
Premier.inhabited [in GroupTheory.g1]
Premier.inv_right_inverse [in GroupTheory.g1]
Premier.inv_left_inverse [in GroupTheory.g1]
Premier.subset [in GroupTheory.g1]
Premier.witness [in GroupTheory.g1]
Q
Quatre.H [in GroupTheory.g2]Quatre.K [in GroupTheory.g2]
Quatre.subH [in GroupTheory.g2]
Quatre.subK [in GroupTheory.g2]
R
Relations.R [in GroupTheory.Relations]Relations.U [in GroupTheory.Relations]
S
Second.eH [in GroupTheory.g1]Second.H [in GroupTheory.g1]
Second.h0 [in GroupTheory.g1]
Second.h1 [in GroupTheory.g1]
Second.h2 [in GroupTheory.g1]
Second.witness [in GroupTheory.g1]
T
Trois.H [in GroupTheory.g2]Trois.K [in GroupTheory.g2]
Trois.subH [in GroupTheory.g2]
Trois.subK [in GroupTheory.g2]
Library Index
G
grGroup_definitions
g1
g2
g3
L
LawsN
Nat_complementsR
RelationsZ
ZaddZbase
Zle
Z_succ_pred
Lemma Index
A
abs_eq_or_oppZ [in GroupTheory.Z.Zadd]addZ_neutral [in GroupTheory.Z.Zadd]
addZ_associativity [in GroupTheory.Z.Zadd]
addZ_commutativity [in GroupTheory.Z.Zadd]
addZ_eq5 [in GroupTheory.Z.Zadd]
addZ_eq4 [in GroupTheory.Z.Zadd]
addZ_eq3 [in GroupTheory.Z.Zadd]
addZ_eq2 [in GroupTheory.Z.Zadd]
addZ_eq1 [in GroupTheory.Z.Zadd]
add_exponents [in GroupTheory.g1]
add_mIZ_predZ [in GroupTheory.Z.Zadd]
add_IZ_succZ [in GroupTheory.Z.Zadd]
add_OZ [in GroupTheory.Z.Zadd]
auxsub [in GroupTheory.g2]
C
cancellation [in GroupTheory.gr]change_exponent_sign [in GroupTheory.g1]
E
eh_is_e [in GroupTheory.g1]eH_in_G [in GroupTheory.g1]
Equiv_from_order [in GroupTheory.Relations]
eq_gt_O_dec [in GroupTheory.Z.Nat_complements]
eq_OZ_dec [in GroupTheory.Z.Zbase]
exp_commut1 [in GroupTheory.g1]
exp_l2' [in GroupTheory.g1]
exp_l2 [in GroupTheory.g1]
exp_l1 [in GroupTheory.g1]
exp_unfold_neg [in GroupTheory.g1]
exp_unfold_pos [in GroupTheory.g1]
exp_endo [in GroupTheory.g1]
Ex1 [in GroupTheory.g1]
Ex2 [in GroupTheory.g1]
Ex3 [in GroupTheory.g1]
Ex4 [in GroupTheory.g1]
Ex5 [in GroupTheory.g1]
I
invH_is_inv [in GroupTheory.g1]inv_endo [in GroupTheory.g1]
inv_involution [in GroupTheory.gr]
inv_star [in GroupTheory.gr]
L
leZ_antisymmetric [in GroupTheory.Z.Zle]le_opp_OZ2 [in GroupTheory.Z.Zle]
le_opp_OZ [in GroupTheory.Z.Zle]
le_opp_OZ_l [in GroupTheory.Z.Zle]
lt_succ [in GroupTheory.Z.Nat_complements]
lt_minus2 [in GroupTheory.Z.Nat_complements]
l1 [in GroupTheory.g1]
M
minus_n_Sm [in GroupTheory.Z.Nat_complements]O
opp_predZ [in GroupTheory.Z.Zadd]opp_succZ [in GroupTheory.Z.Zadd]
P
phi_exp [in GroupTheory.g3]phi_unfold [in GroupTheory.g3]
positive_powers [in GroupTheory.g3]
powers_of_one_element [in GroupTheory.g1]
powers_repeat [in GroupTheory.g3]
pred_succZ [in GroupTheory.Z.Z_succ_pred]
pred_addZ_r [in GroupTheory.Z.Zadd]
pred_addZ_l [in GroupTheory.Z.Zadd]
psi_not_inj [in GroupTheory.g3]
R
remaining [in GroupTheory.g3]resolve [in GroupTheory.gr]
S
self_inv [in GroupTheory.gr]sign_absZ [in GroupTheory.Z.Zle]
starH_is_star [in GroupTheory.g1]
star_endo [in GroupTheory.g1]
Subgroup_inhabited [in GroupTheory.g1]
succ_pred_pred_succZ [in GroupTheory.Z.Z_succ_pred]
succ_predZ [in GroupTheory.Z.Z_succ_pred]
succ_addZ_r [in GroupTheory.Z.Zadd]
succ_addZ_l [in GroupTheory.Z.Zadd]
sym_not_P [in GroupTheory.Relations]
T
technical_lemma [in GroupTheory.Z.Nat_complements]tech_opp_pos_negZ2 [in GroupTheory.g1]
tech_opp_pos_negZ1 [in GroupTheory.g1]
tech_posOZ_pos [in GroupTheory.Z.Zle]
tech_lt_abs_OZ [in GroupTheory.Z.Zle]
tech_le_pos_abs [in GroupTheory.Z.Zle]
tech_succ_posOZ [in GroupTheory.Z.Z_succ_pred]
tech_pred_posZ [in GroupTheory.Z.Z_succ_pred]
tech_pos_not_posZ [in GroupTheory.Z.Zbase]
tech_opp_pos_negZ [in GroupTheory.Z.Zadd]
tech_add_neg_negZ [in GroupTheory.Z.Zadd]
tech_add_pos_posZ [in GroupTheory.Z.Zadd]
tech_add_neg_posZ [in GroupTheory.Z.Zadd]
tech_add_pos_negZ [in GroupTheory.Z.Zadd]
tech_add_pos_neg_posZ [in GroupTheory.Z.Zadd]
tech_add_neg_predZ [in GroupTheory.Z.Zadd]
tech_add_pos_succZ [in GroupTheory.Z.Zadd]
tech_exp' [in GroupTheory.g3]
tech_exp [in GroupTheory.g3]
triv1 [in GroupTheory.gr]
triv2 [in GroupTheory.gr]
T_1_6_3 [in GroupTheory.g1]
T_1_6_2 [in GroupTheory.g1]
T_1_6_8 [in GroupTheory.g2]
T_1_6_4 [in GroupTheory.g3]
T4 [in GroupTheory.g2]
T4R [in GroupTheory.g2]
T4R1 [in GroupTheory.g2]
Constructor Index
D
Definition_of_Prod [in GroupTheory.g2]Definition_of_subgroup [in GroupTheory.Group_definitions]
G
group [in GroupTheory.Group_definitions]I
In_powers [in GroupTheory.g1]N
neg [in GroupTheory.Z.Zbase]O
OZ [in GroupTheory.Z.Zbase]P
pos [in GroupTheory.Z.Zbase]Axiom Index
G
Gr [in GroupTheory.g1]U
U [in GroupTheory.g1]Inductive Index
P
powers [in GroupTheory.g1]Prod [in GroupTheory.g2]
S
subgroup [in GroupTheory.Group_definitions]Z
Z [in GroupTheory.Z.Zbase]Projection Index
E
e_ [in GroupTheory.Group_definitions]G
G_ [in GroupTheory.Group_definitions]G0_ [in GroupTheory.Group_definitions]
G1_ [in GroupTheory.Group_definitions]
G2a_ [in GroupTheory.Group_definitions]
G2b_ [in GroupTheory.Group_definitions]
G2c_ [in GroupTheory.Group_definitions]
G3a_ [in GroupTheory.Group_definitions]
G3b_ [in GroupTheory.Group_definitions]
G3c_ [in GroupTheory.Group_definitions]
I
inv_ [in GroupTheory.Group_definitions]S
star_ [in GroupTheory.Group_definitions]Section Index
B
Basic_laws [in GroupTheory.Laws]C
Cinq [in GroupTheory.g3]E
Elements [in GroupTheory.g1]G
group_trivialities [in GroupTheory.gr]group_definition [in GroupTheory.Group_definitions]
P
Premier [in GroupTheory.g1]Q
Quatre [in GroupTheory.g2]R
Relations [in GroupTheory.Relations]S
Second [in GroupTheory.g1]T
Trois [in GroupTheory.g2]Definition Index
A
absZ [in GroupTheory.Z.Zbase]addZ [in GroupTheory.Z.Zadd]
add1 [in GroupTheory.Z.Zadd]
add2 [in GroupTheory.Z.Zadd]
Antisymmetric [in GroupTheory.Relations]
associative [in GroupTheory.Z.Zadd]
associative [in GroupTheory.Laws]
C
cancellation' [in GroupTheory.g1]commutative [in GroupTheory.Z.Zadd]
commutative [in GroupTheory.Laws]
E
e [in GroupTheory.g1]endo_operation [in GroupTheory.Laws]
endo_function [in GroupTheory.Laws]
Equivalence [in GroupTheory.Relations]
exp [in GroupTheory.g1]
G
G [in GroupTheory.g1]G0 [in GroupTheory.gr]
G0' [in GroupTheory.g1]
G1 [in GroupTheory.gr]
G1' [in GroupTheory.g1]
G2a [in GroupTheory.gr]
G2a' [in GroupTheory.g1]
G2b [in GroupTheory.gr]
G2b' [in GroupTheory.g1]
G2c [in GroupTheory.gr]
G2c' [in GroupTheory.g1]
G3a [in GroupTheory.gr]
G3a' [in GroupTheory.g1]
G3b [in GroupTheory.gr]
G3b' [in GroupTheory.g1]
G3c [in GroupTheory.gr]
G3c' [in GroupTheory.g1]
I
IdZ [in GroupTheory.Z.Zadd]inv [in GroupTheory.g1]
inv_involution' [in GroupTheory.g1]
inv_star' [in GroupTheory.g1]
is_posn [in GroupTheory.Z.Zbase]
IZ [in GroupTheory.Z.Zbase]
L
left_inverse [in GroupTheory.Laws]left_neutral [in GroupTheory.Laws]
leZ [in GroupTheory.Z.Zle]
ltZ [in GroupTheory.Z.Zle]
lt_absZ [in GroupTheory.Z.Zle]
N
negOZ [in GroupTheory.Z.Zbase]neutral [in GroupTheory.Z.Zadd]
O
oppZ [in GroupTheory.Z.Zadd]Order [in GroupTheory.Relations]
P
PER [in GroupTheory.Relations]phi [in GroupTheory.g3]
posOZ [in GroupTheory.Z.Zbase]
predZ [in GroupTheory.Z.Z_succ_pred]
psi [in GroupTheory.g3]
R
Reflexive [in GroupTheory.Relations]Relation [in GroupTheory.Relations]
resolve' [in GroupTheory.g1]
right_inverse [in GroupTheory.Laws]
right_neutral [in GroupTheory.Laws]
S
self_inv' [in GroupTheory.g1]Setsubgroup [in GroupTheory.Group_definitions]
sgnZ [in GroupTheory.Z.Zbase]
star [in GroupTheory.g1]
succZ [in GroupTheory.Z.Z_succ_pred]
Symmetric [in GroupTheory.Relations]
T
Transitive [in GroupTheory.Relations]triv1' [in GroupTheory.g1]
triv2' [in GroupTheory.g1]
Record Index
G
Group [in GroupTheory.Group_definitions]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (259 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (96 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (66 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |