| 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 | (221 entries) |
| Notation 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 | (11 entries) |
| Module 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 | (3 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 | (7 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 | (8 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 | (52 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 | (2 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 | (47 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 | (2 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 | (12 entries) |
| Instance 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 | (13 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 | (51 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 | (13 entries) |
Global Index
A
Abelian_Group [record, in CoMoAlg.Groups]action [projection, in CoMoAlg.Groups.Actions]
Action [record, in CoMoAlg.Groups.Actions]
Actions [library]
action_equiv [instance, in CoMoAlg.Groups.Actions]
action_assoc [projection, in CoMoAlg.Groups.Actions]
action_neutr [projection, in CoMoAlg.Groups.Actions]
action_compat [projection, in CoMoAlg.Groups.Actions]
addQ [definition, in CoMoAlg.Fields.Constructions]
addQ_comm [lemma, in CoMoAlg.Fields.Constructions]
addQ_assoc [lemma, in CoMoAlg.Fields.Constructions]
addQ_compat [instance, in CoMoAlg.Fields.Constructions]
Auto_Group [definition, in CoMoAlg.Groups]
B
base_Setoid_Morph [projection, in CoMoAlg.Groups]base_Group [projection, in CoMoAlg.Groups]
base_Setoid [projection, in CoMoAlg.Groups]
base_Ring [projection, in CoMoAlg.Rings]
base_Abelian [projection, in CoMoAlg.Rings]
base_Field [projection, in CoMoAlg.Fields]
base_Integrity_Ring [projection, in CoMoAlg.Fields]
bijective [definition, in CoMoAlg.Setoids]
bijective_surjective [lemma, in CoMoAlg.Setoids]
bijective_injective [lemma, in CoMoAlg.Setoids]
Build_Morph' [definition, in CoMoAlg.Groups]
Build_Abelian_Group' [definition, in CoMoAlg.Groups]
Build_Group' [definition, in CoMoAlg.Groups]
C
carr [projection, in CoMoAlg.Setoids]carreq [projection, in CoMoAlg.Setoids]
carreq_equiv [projection, in CoMoAlg.Setoids]
carr_inhabited [lemma, in CoMoAlg.Groups]
commutative [projection, in CoMoAlg.Rings]
Commutative_Ring [record, in CoMoAlg.Rings]
comp [definition, in CoMoAlg.Groups]
comparability [lemma, in CoMoAlg.Fields]
comparability_eq [lemma, in CoMoAlg.Fields]
comparing [section, in CoMoAlg.Fields]
_ <= _ (ring_scope) [notation, in CoMoAlg.Fields]
_ < _ (ring_scope) [notation, in CoMoAlg.Fields]
_ >= _ (ring_scope) [notation, in CoMoAlg.Fields]
_ > _ (ring_scope) [notation, in CoMoAlg.Fields]
Constructions [library]
E
easier [section, in CoMoAlg.Groups.Subgroup]easier.H1 [variable, in CoMoAlg.Groups.Subgroup]
easier.H2 [variable, in CoMoAlg.Groups.Subgroup]
easier.H3 [variable, in CoMoAlg.Groups.Subgroup]
equivariance [projection, in CoMoAlg.Groups.Actions]
Equivariance [record, in CoMoAlg.Groups.Actions]
equivariance_action [projection, in CoMoAlg.Groups.Actions]
equivariance_compat [projection, in CoMoAlg.Groups.Actions]
equiv_Morph_inj [definition, in CoMoAlg.Groups.Quotients]
equiv_Morph_surj [definition, in CoMoAlg.Groups.Quotients]
equiv_Group [instance, in CoMoAlg.Groups.Quotients]
F
Field [record, in CoMoAlg.Fields]Fields [library]
Field_Properties [section, in CoMoAlg.Fields]
G
ge [definition, in CoMoAlg.Fields]Group [record, in CoMoAlg.Groups]
Groups [library]
Group_Morph_trivial.trivial_Morph [instance, in CoMoAlg.Groups]
Group_Morph_trivial [module, in CoMoAlg.Groups]
Group_Morph [record, in CoMoAlg.Groups]
Group_Properties [section, in CoMoAlg.Groups]
gt [definition, in CoMoAlg.Fields]
gt_mul [lemma, in CoMoAlg.Fields]
gt_neg [lemma, in CoMoAlg.Fields]
gt_compat [instance, in CoMoAlg.Fields]
I
injective [definition, in CoMoAlg.Setoids]injective_surjective_bijective [lemma, in CoMoAlg.Setoids]
Integers [module, in CoMoAlg.Groups]
Integers.addZ [definition, in CoMoAlg.Groups]
Integers.diffeq [inductive, in CoMoAlg.Groups]
Integers.diffeq_0 [lemma, in CoMoAlg.Groups]
Integers.diffeq_sind [definition, in CoMoAlg.Groups]
Integers.diffeq_ind [definition, in CoMoAlg.Groups]
Integers.diffeq_1 [constructor, in CoMoAlg.Groups]
Integers.invZ [definition, in CoMoAlg.Groups]
Integers.Z [definition, in CoMoAlg.Groups]
Integers.Z_Group [instance, in CoMoAlg.Groups]
Integers.Z0 [definition, in CoMoAlg.Groups]
Integrity_Ring_Properties [section, in CoMoAlg.Rings]
Integrity_Ring [record, in CoMoAlg.Rings]
inv [projection, in CoMoAlg.Groups]
invM [projection, in CoMoAlg.Fields]
invM_unique [lemma, in CoMoAlg.Fields]
invQ [definition, in CoMoAlg.Fields.Constructions]
inv_compat [instance, in CoMoAlg.Groups]
inv_inv [lemma, in CoMoAlg.Groups]
inv_op [lemma, in CoMoAlg.Groups]
inv_neutr [lemma, in CoMoAlg.Groups]
inv_unique [lemma, in CoMoAlg.Groups]
inv_preserve' [lemma, in CoMoAlg.Groups.Subgroup]
L
le [definition, in CoMoAlg.Fields]le_ge_eq [lemma, in CoMoAlg.Fields]
lt [definition, in CoMoAlg.Fields]
lt_mul [lemma, in CoMoAlg.Fields]
lt_add [lemma, in CoMoAlg.Fields]
lt_transitive [lemma, in CoMoAlg.Fields]
M
max [definition, in CoMoAlg.Fields]max_unique [lemma, in CoMoAlg.Fields]
min [definition, in CoMoAlg.Fields]
min_unique [lemma, in CoMoAlg.Fields]
morph [projection, in CoMoAlg.Setoids]
morph_inv [lemma, in CoMoAlg.Groups]
morph_neutr [lemma, in CoMoAlg.Groups]
Morph_Properties [section, in CoMoAlg.Groups]
morph_op [projection, in CoMoAlg.Groups]
morph_compat [projection, in CoMoAlg.Setoids]
mul [projection, in CoMoAlg.Rings]
mulQ [definition, in CoMoAlg.Fields.Constructions]
mulQ_addQ_distr_2 [lemma, in CoMoAlg.Fields.Constructions]
mulQ_addQ_distr_1 [lemma, in CoMoAlg.Fields.Constructions]
mulQ_comm [lemma, in CoMoAlg.Fields.Constructions]
mulQ_compat [instance, in CoMoAlg.Fields.Constructions]
mul_neq_0 [lemma, in CoMoAlg.Rings]
mul_0 [lemma, in CoMoAlg.Rings]
mul_comm [projection, in CoMoAlg.Rings]
mul_one_l [projection, in CoMoAlg.Rings]
mul_inv_r [lemma, in CoMoAlg.Rings]
mul_inv_l [lemma, in CoMoAlg.Rings]
mul_0_r [lemma, in CoMoAlg.Rings]
mul_0_l [lemma, in CoMoAlg.Rings]
mul_op_distr_2 [projection, in CoMoAlg.Rings]
mul_op_distr_1 [projection, in CoMoAlg.Rings]
mul_assoc [projection, in CoMoAlg.Rings]
mul_compat [projection, in CoMoAlg.Rings]
mul_div_l [projection, in CoMoAlg.Fields]
N
neutr [projection, in CoMoAlg.Groups]neutr_unique [lemma, in CoMoAlg.Groups]
neutr_preserve' [lemma, in CoMoAlg.Groups.Subgroup]
Noether [section, in CoMoAlg.Groups.Quotients]
Noether_inj [lemma, in CoMoAlg.Groups.Quotients]
Noether_commut [lemma, in CoMoAlg.Groups.Quotients]
not_0_unit [lemma, in CoMoAlg.Fields]
O
one [projection, in CoMoAlg.Rings]one_neq_0 [projection, in CoMoAlg.Rings]
one_unit [definition, in CoMoAlg.Rings]
one_gt_0 [lemma, in CoMoAlg.Fields]
one_unique [lemma, in CoMoAlg.Fields]
op [projection, in CoMoAlg.Groups]
op_comm [projection, in CoMoAlg.Groups]
op_neutr_r [lemma, in CoMoAlg.Groups]
op_inv_r [lemma, in CoMoAlg.Groups]
op_inv_l [projection, in CoMoAlg.Groups]
op_neutr_l [projection, in CoMoAlg.Groups]
op_assoc [projection, in CoMoAlg.Groups]
op_compat [projection, in CoMoAlg.Groups]
op_preserve' [lemma, in CoMoAlg.Groups.Subgroup]
orbit [definition, in CoMoAlg.Groups.Actions]
Ordered_Field [record, in CoMoAlg.Fields]
P
positive [projection, in CoMoAlg.Fields]positive_mul [projection, in CoMoAlg.Fields]
positive_add [projection, in CoMoAlg.Fields]
positive_cases [projection, in CoMoAlg.Fields]
positive_compat [projection, in CoMoAlg.Fields]
predicates [section, in CoMoAlg.Setoids]
Q
quadr_gt_0 [lemma, in CoMoAlg.Fields]quoteq [inductive, in CoMoAlg.Fields.Constructions]
quoteq_equiv [instance, in CoMoAlg.Fields.Constructions]
quoteq_sind [definition, in CoMoAlg.Fields.Constructions]
quoteq_ind [definition, in CoMoAlg.Fields.Constructions]
quoteq_1 [constructor, in CoMoAlg.Fields.Constructions]
Quotients [library]
Quot_Field [definition, in CoMoAlg.Fields.Constructions]
Quot_Integrity_Ring [definition, in CoMoAlg.Fields.Constructions]
Quot_Unital_Ring [definition, in CoMoAlg.Fields.Constructions]
Quot_Commutative_Ring [definition, in CoMoAlg.Fields.Constructions]
Quot_Ring [definition, in CoMoAlg.Fields.Constructions]
Quot_Abelian_Group [definition, in CoMoAlg.Fields.Constructions]
Quot_Group [definition, in CoMoAlg.Fields.Constructions]
Quot_Setoid [definition, in CoMoAlg.Fields.Constructions]
quot_field.Q [variable, in CoMoAlg.Fields.Constructions]
quot_field [section, in CoMoAlg.Fields.Constructions]
Q0 [definition, in CoMoAlg.Fields.Constructions]
Q1 [definition, in CoMoAlg.Fields.Constructions]
R
Ring [record, in CoMoAlg.Rings]Rings [library]
Ring_Properties [section, in CoMoAlg.Rings]
S
Setoid [record, in CoMoAlg.Setoids]Setoids [library]
Setoid_Morph [record, in CoMoAlg.Setoids]
shorten_r [lemma, in CoMoAlg.Groups]
shorten_l [lemma, in CoMoAlg.Groups]
Subgroup [instance, in CoMoAlg.Groups.Subgroup]
subgroup [section, in CoMoAlg.Groups.Subgroup]
Subgroup [library]
subgroup.inv_preserve [variable, in CoMoAlg.Groups.Subgroup]
subgroup.neutr_preserve [variable, in CoMoAlg.Groups.Subgroup]
subgroup.op_preserve [variable, in CoMoAlg.Groups.Subgroup]
subset_gt [definition, in CoMoAlg.Fields]
subset_lt [definition, in CoMoAlg.Fields]
subset_ge [definition, in CoMoAlg.Fields]
subset_le [definition, in CoMoAlg.Fields]
subset_mul [definition, in CoMoAlg.Fields]
subset_add_assoc [lemma, in CoMoAlg.Fields]
subset_add_comm [lemma, in CoMoAlg.Fields]
subset_add [definition, in CoMoAlg.Fields]
surjective [definition, in CoMoAlg.Setoids]
T
trivial_Action_orbit [definition, in CoMoAlg.Groups.Actions]trivial_Action [instance, in CoMoAlg.Groups.Actions]
U
unit [definition, in CoMoAlg.Rings]unital [projection, in CoMoAlg.Rings]
Unital_Ring [record, in CoMoAlg.Rings]
units [section, in CoMoAlg.Rings]
unit_one_unique [lemma, in CoMoAlg.Rings]
unit_mul_one_r [lemma, in CoMoAlg.Rings]
unit_Group [definition, in CoMoAlg.Rings]
unit_Setoid [definition, in CoMoAlg.Rings]
unit_not_0 [lemma, in CoMoAlg.Fields]
Z
Z [module, in CoMoAlg.Rings]zero_divisor_free [projection, in CoMoAlg.Rings]
zero_divisor [definition, in CoMoAlg.Rings]
Z.mulZ [definition, in CoMoAlg.Rings]
Z.Z_Integrity_Ring [instance, in CoMoAlg.Rings]
Z.Z_Ring [instance, in CoMoAlg.Rings]
other
- _ (abelian_scope) [notation, in CoMoAlg.Groups]_ + _ (abelian_scope) [notation, in CoMoAlg.Groups]
_ * _ (group_scope) [notation, in CoMoAlg.Groups]
1 (ring_scope) [notation, in CoMoAlg.Rings]
0 (ring_scope) [notation, in CoMoAlg.Rings]
_ * _ (ring_scope) [notation, in CoMoAlg.Rings]
_ =s= _ (setoid_scope) [notation, in CoMoAlg.Setoids]
Notation Index
C
_ <= _ (ring_scope) [in CoMoAlg.Fields]_ < _ (ring_scope) [in CoMoAlg.Fields]
_ >= _ (ring_scope) [in CoMoAlg.Fields]
_ > _ (ring_scope) [in CoMoAlg.Fields]
other
- _ (abelian_scope) [in CoMoAlg.Groups]_ + _ (abelian_scope) [in CoMoAlg.Groups]
_ * _ (group_scope) [in CoMoAlg.Groups]
1 (ring_scope) [in CoMoAlg.Rings]
0 (ring_scope) [in CoMoAlg.Rings]
_ * _ (ring_scope) [in CoMoAlg.Rings]
_ =s= _ (setoid_scope) [in CoMoAlg.Setoids]
Module Index
G
Group_Morph_trivial [in CoMoAlg.Groups]I
Integers [in CoMoAlg.Groups]Z
Z [in CoMoAlg.Rings]Variable Index
E
easier.H1 [in CoMoAlg.Groups.Subgroup]easier.H2 [in CoMoAlg.Groups.Subgroup]
easier.H3 [in CoMoAlg.Groups.Subgroup]
Q
quot_field.Q [in CoMoAlg.Fields.Constructions]S
subgroup.inv_preserve [in CoMoAlg.Groups.Subgroup]subgroup.neutr_preserve [in CoMoAlg.Groups.Subgroup]
subgroup.op_preserve [in CoMoAlg.Groups.Subgroup]
Library Index
A
ActionsC
ConstructionsF
FieldsG
GroupsQ
QuotientsR
RingsS
SetoidsSubgroup
Lemma Index
A
addQ_comm [in CoMoAlg.Fields.Constructions]addQ_assoc [in CoMoAlg.Fields.Constructions]
B
bijective_surjective [in CoMoAlg.Setoids]bijective_injective [in CoMoAlg.Setoids]
C
carr_inhabited [in CoMoAlg.Groups]comparability [in CoMoAlg.Fields]
comparability_eq [in CoMoAlg.Fields]
G
gt_mul [in CoMoAlg.Fields]gt_neg [in CoMoAlg.Fields]
I
injective_surjective_bijective [in CoMoAlg.Setoids]Integers.diffeq_0 [in CoMoAlg.Groups]
invM_unique [in CoMoAlg.Fields]
inv_inv [in CoMoAlg.Groups]
inv_op [in CoMoAlg.Groups]
inv_neutr [in CoMoAlg.Groups]
inv_unique [in CoMoAlg.Groups]
inv_preserve' [in CoMoAlg.Groups.Subgroup]
L
le_ge_eq [in CoMoAlg.Fields]lt_mul [in CoMoAlg.Fields]
lt_add [in CoMoAlg.Fields]
lt_transitive [in CoMoAlg.Fields]
M
max_unique [in CoMoAlg.Fields]min_unique [in CoMoAlg.Fields]
morph_inv [in CoMoAlg.Groups]
morph_neutr [in CoMoAlg.Groups]
mulQ_addQ_distr_2 [in CoMoAlg.Fields.Constructions]
mulQ_addQ_distr_1 [in CoMoAlg.Fields.Constructions]
mulQ_comm [in CoMoAlg.Fields.Constructions]
mul_neq_0 [in CoMoAlg.Rings]
mul_0 [in CoMoAlg.Rings]
mul_inv_r [in CoMoAlg.Rings]
mul_inv_l [in CoMoAlg.Rings]
mul_0_r [in CoMoAlg.Rings]
mul_0_l [in CoMoAlg.Rings]
N
neutr_unique [in CoMoAlg.Groups]neutr_preserve' [in CoMoAlg.Groups.Subgroup]
Noether_inj [in CoMoAlg.Groups.Quotients]
Noether_commut [in CoMoAlg.Groups.Quotients]
not_0_unit [in CoMoAlg.Fields]
O
one_gt_0 [in CoMoAlg.Fields]one_unique [in CoMoAlg.Fields]
op_neutr_r [in CoMoAlg.Groups]
op_inv_r [in CoMoAlg.Groups]
op_preserve' [in CoMoAlg.Groups.Subgroup]
Q
quadr_gt_0 [in CoMoAlg.Fields]S
shorten_r [in CoMoAlg.Groups]shorten_l [in CoMoAlg.Groups]
subset_add_assoc [in CoMoAlg.Fields]
subset_add_comm [in CoMoAlg.Fields]
U
unit_one_unique [in CoMoAlg.Rings]unit_mul_one_r [in CoMoAlg.Rings]
unit_not_0 [in CoMoAlg.Fields]
Constructor Index
I
Integers.diffeq_1 [in CoMoAlg.Groups]Q
quoteq_1 [in CoMoAlg.Fields.Constructions]Projection Index
A
action [in CoMoAlg.Groups.Actions]action_assoc [in CoMoAlg.Groups.Actions]
action_neutr [in CoMoAlg.Groups.Actions]
action_compat [in CoMoAlg.Groups.Actions]
B
base_Setoid_Morph [in CoMoAlg.Groups]base_Group [in CoMoAlg.Groups]
base_Setoid [in CoMoAlg.Groups]
base_Ring [in CoMoAlg.Rings]
base_Abelian [in CoMoAlg.Rings]
base_Field [in CoMoAlg.Fields]
base_Integrity_Ring [in CoMoAlg.Fields]
C
carr [in CoMoAlg.Setoids]carreq [in CoMoAlg.Setoids]
carreq_equiv [in CoMoAlg.Setoids]
commutative [in CoMoAlg.Rings]
E
equivariance [in CoMoAlg.Groups.Actions]equivariance_action [in CoMoAlg.Groups.Actions]
equivariance_compat [in CoMoAlg.Groups.Actions]
I
inv [in CoMoAlg.Groups]invM [in CoMoAlg.Fields]
M
morph [in CoMoAlg.Setoids]morph_op [in CoMoAlg.Groups]
morph_compat [in CoMoAlg.Setoids]
mul [in CoMoAlg.Rings]
mul_comm [in CoMoAlg.Rings]
mul_one_l [in CoMoAlg.Rings]
mul_op_distr_2 [in CoMoAlg.Rings]
mul_op_distr_1 [in CoMoAlg.Rings]
mul_assoc [in CoMoAlg.Rings]
mul_compat [in CoMoAlg.Rings]
mul_div_l [in CoMoAlg.Fields]
N
neutr [in CoMoAlg.Groups]O
one [in CoMoAlg.Rings]one_neq_0 [in CoMoAlg.Rings]
op [in CoMoAlg.Groups]
op_comm [in CoMoAlg.Groups]
op_inv_l [in CoMoAlg.Groups]
op_neutr_l [in CoMoAlg.Groups]
op_assoc [in CoMoAlg.Groups]
op_compat [in CoMoAlg.Groups]
P
positive [in CoMoAlg.Fields]positive_mul [in CoMoAlg.Fields]
positive_add [in CoMoAlg.Fields]
positive_cases [in CoMoAlg.Fields]
positive_compat [in CoMoAlg.Fields]
U
unital [in CoMoAlg.Rings]Z
zero_divisor_free [in CoMoAlg.Rings]Inductive Index
I
Integers.diffeq [in CoMoAlg.Groups]Q
quoteq [in CoMoAlg.Fields.Constructions]Section Index
C
comparing [in CoMoAlg.Fields]E
easier [in CoMoAlg.Groups.Subgroup]F
Field_Properties [in CoMoAlg.Fields]G
Group_Properties [in CoMoAlg.Groups]I
Integrity_Ring_Properties [in CoMoAlg.Rings]M
Morph_Properties [in CoMoAlg.Groups]N
Noether [in CoMoAlg.Groups.Quotients]P
predicates [in CoMoAlg.Setoids]Q
quot_field [in CoMoAlg.Fields.Constructions]R
Ring_Properties [in CoMoAlg.Rings]S
subgroup [in CoMoAlg.Groups.Subgroup]U
units [in CoMoAlg.Rings]Instance Index
A
action_equiv [in CoMoAlg.Groups.Actions]addQ_compat [in CoMoAlg.Fields.Constructions]
E
equiv_Group [in CoMoAlg.Groups.Quotients]G
Group_Morph_trivial.trivial_Morph [in CoMoAlg.Groups]gt_compat [in CoMoAlg.Fields]
I
Integers.Z_Group [in CoMoAlg.Groups]inv_compat [in CoMoAlg.Groups]
M
mulQ_compat [in CoMoAlg.Fields.Constructions]Q
quoteq_equiv [in CoMoAlg.Fields.Constructions]S
Subgroup [in CoMoAlg.Groups.Subgroup]T
trivial_Action [in CoMoAlg.Groups.Actions]Z
Z.Z_Integrity_Ring [in CoMoAlg.Rings]Z.Z_Ring [in CoMoAlg.Rings]
Definition Index
A
addQ [in CoMoAlg.Fields.Constructions]Auto_Group [in CoMoAlg.Groups]
B
bijective [in CoMoAlg.Setoids]Build_Morph' [in CoMoAlg.Groups]
Build_Abelian_Group' [in CoMoAlg.Groups]
Build_Group' [in CoMoAlg.Groups]
C
comp [in CoMoAlg.Groups]E
equiv_Morph_inj [in CoMoAlg.Groups.Quotients]equiv_Morph_surj [in CoMoAlg.Groups.Quotients]
G
ge [in CoMoAlg.Fields]gt [in CoMoAlg.Fields]
I
injective [in CoMoAlg.Setoids]Integers.addZ [in CoMoAlg.Groups]
Integers.diffeq_sind [in CoMoAlg.Groups]
Integers.diffeq_ind [in CoMoAlg.Groups]
Integers.invZ [in CoMoAlg.Groups]
Integers.Z [in CoMoAlg.Groups]
Integers.Z0 [in CoMoAlg.Groups]
invQ [in CoMoAlg.Fields.Constructions]
L
le [in CoMoAlg.Fields]lt [in CoMoAlg.Fields]
M
max [in CoMoAlg.Fields]min [in CoMoAlg.Fields]
mulQ [in CoMoAlg.Fields.Constructions]
O
one_unit [in CoMoAlg.Rings]orbit [in CoMoAlg.Groups.Actions]
Q
quoteq_sind [in CoMoAlg.Fields.Constructions]quoteq_ind [in CoMoAlg.Fields.Constructions]
Quot_Field [in CoMoAlg.Fields.Constructions]
Quot_Integrity_Ring [in CoMoAlg.Fields.Constructions]
Quot_Unital_Ring [in CoMoAlg.Fields.Constructions]
Quot_Commutative_Ring [in CoMoAlg.Fields.Constructions]
Quot_Ring [in CoMoAlg.Fields.Constructions]
Quot_Abelian_Group [in CoMoAlg.Fields.Constructions]
Quot_Group [in CoMoAlg.Fields.Constructions]
Quot_Setoid [in CoMoAlg.Fields.Constructions]
Q0 [in CoMoAlg.Fields.Constructions]
Q1 [in CoMoAlg.Fields.Constructions]
S
subset_gt [in CoMoAlg.Fields]subset_lt [in CoMoAlg.Fields]
subset_ge [in CoMoAlg.Fields]
subset_le [in CoMoAlg.Fields]
subset_mul [in CoMoAlg.Fields]
subset_add [in CoMoAlg.Fields]
surjective [in CoMoAlg.Setoids]
T
trivial_Action_orbit [in CoMoAlg.Groups.Actions]U
unit [in CoMoAlg.Rings]unit_Group [in CoMoAlg.Rings]
unit_Setoid [in CoMoAlg.Rings]
Z
zero_divisor [in CoMoAlg.Rings]Z.mulZ [in CoMoAlg.Rings]
Record Index
A
Abelian_Group [in CoMoAlg.Groups]Action [in CoMoAlg.Groups.Actions]
C
Commutative_Ring [in CoMoAlg.Rings]E
Equivariance [in CoMoAlg.Groups.Actions]F
Field [in CoMoAlg.Fields]G
Group [in CoMoAlg.Groups]Group_Morph [in CoMoAlg.Groups]
I
Integrity_Ring [in CoMoAlg.Rings]O
Ordered_Field [in CoMoAlg.Fields]R
Ring [in CoMoAlg.Rings]S
Setoid [in CoMoAlg.Setoids]Setoid_Morph [in CoMoAlg.Setoids]
U
Unital_Ring [in CoMoAlg.Rings]| 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 | (221 entries) |
| Notation 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 | (11 entries) |
| Module 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 | (3 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 | (7 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 | (8 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 | (52 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 | (2 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 | (47 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 | (2 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 | (12 entries) |
| Instance 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 | (13 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 | (51 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 | (13 entries) |