| 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 | (1509 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 | (352 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 | (72 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 | (419 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 | (72 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 | (18 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 | (11 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 | (112 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 | (125 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 | (280 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 | (48 entries) |
Global Index
A
Abelian_group.fcom [variable, in Algebra.Group_util]Abelian_group.geninvr [variable, in Algebra.Group_util]
Abelian_group.invcomp [variable, in Algebra.Group_util]
Abelian_group.eunitgenlawr [variable, in Algebra.Group_util]
Abelian_group.genlawassoc [variable, in Algebra.Group_util]
Abelian_group.fcomp [variable, in Algebra.Group_util]
Abelian_group.geninv [variable, in Algebra.Group_util]
Abelian_group.e [variable, in Algebra.Group_util]
Abelian_group.genlaw [variable, in Algebra.Group_util]
Abelian_group.E [variable, in Algebra.Group_util]
Abelian_group [section, in Algebra.Group_util]
ABELIAN_GROUP [definition, in Algebra.Abelian_group_cat]
abelian_group_on_def [projection, in Algebra.Abelian_group_cat]
abelian_group_group [projection, in Algebra.Abelian_group_cat]
abelian_group [record, in Algebra.Abelian_group_cat]
abelian_group_abelian_monoid [projection, in Algebra.Abelian_group_cat]
abelian_group_on [record, in Algebra.Abelian_group_cat]
ABELIAN_MONOID [definition, in Algebra.Abelian_group_cat]
abelian_monoid_on_def [projection, in Algebra.Abelian_group_cat]
abelian_monoid_monoid [projection, in Algebra.Abelian_group_cat]
abelian_monoid [record, in Algebra.Abelian_group_cat]
abelian_monoid_abelian_sgroup [projection, in Algebra.Abelian_group_cat]
abelian_monoid_on [record, in Algebra.Abelian_group_cat]
ABELIAN_SGROUP [definition, in Algebra.Abelian_group_cat]
abelian_sgroup_on_def [projection, in Algebra.Abelian_group_cat]
abelian_sgroup_sgroup [projection, in Algebra.Abelian_group_cat]
abelian_sgroup [record, in Algebra.Abelian_group_cat]
abelian_sgroup_com_prf [projection, in Algebra.Abelian_group_cat]
abelian_sgroup_on [record, in Algebra.Abelian_group_cat]
ABELIAN_GROUP4 [lemma, in Algebra.Abelian_group_facts]
ABELIAN_GROUP_permute [lemma, in Algebra.Abelian_group_facts]
ABELIAN_GROUP_com [lemma, in Algebra.Abelian_group_facts]
ABELIAN_MONOID4 [lemma, in Algebra.Abelian_group_facts]
ABELIAN_MONOID_permute [lemma, in Algebra.Abelian_group_facts]
ABELIAN_MONOID_com [lemma, in Algebra.Abelian_group_facts]
ABELIAN_SGROUP4 [lemma, in Algebra.Abelian_group_facts]
ABELIAN_SGROUP_permute [lemma, in Algebra.Abelian_group_facts]
ABELIAN_SGROUP_com [lemma, in Algebra.Abelian_group_facts]
Abelian_monoid.fcom [variable, in Algebra.Monoid_util]
Abelian_monoid.eunitgenlawl [variable, in Algebra.Monoid_util]
Abelian_monoid.eunitgenlawr [variable, in Algebra.Monoid_util]
Abelian_monoid.genlawassoc [variable, in Algebra.Monoid_util]
Abelian_monoid.fcomp [variable, in Algebra.Monoid_util]
Abelian_monoid.e [variable, in Algebra.Monoid_util]
Abelian_monoid.genlaw [variable, in Algebra.Monoid_util]
Abelian_monoid.E [variable, in Algebra.Monoid_util]
Abelian_monoid [section, in Algebra.Monoid_util]
Abelian_group_cat [library]
Abelian_group_facts [library]
addfraction_law [lemma, in Algebra.Fraction_field]
addfraction_law_r [lemma, in Algebra.Fraction_field]
addfraction_fun_com [lemma, in Algebra.Fraction_field]
addfraction_law_l [lemma, in Algebra.Fraction_field]
addfraction_fun [definition, in Algebra.Fraction_field]
add_hom_module [definition, in Algebra.Hom_module]
add_minus [lemma, in Algebra.Fpart]
add_part_simpl [lemma, in Algebra.Fpart]
add_part_in_el_not_in [lemma, in Algebra.Fpart]
add_part_in_el_diff [lemma, in Algebra.Fpart]
add_in [lemma, in Algebra.Fpart]
add_part_com [lemma, in Algebra.Fpart]
add_part_in [lemma, in Algebra.Fpart]
add_part_comp [lemma, in Algebra.Fpart]
add_part [definition, in Algebra.Fpart]
algebra [record, in Algebra.Algebra]
Algebra [library]
ALGEBRA_mult_lin_left [axiom, in Algebra.Algebra_facts]
ALGEBRA_mult_lin_right [lemma, in Algebra.Algebra_facts]
ALGEBRA_lin_left [axiom, in Algebra.Algebra_facts]
ALGEBRA_lin_right [lemma, in Algebra.Algebra_facts]
ALGEBRA_comp [lemma, in Algebra.Algebra_facts]
algebra_mult [definition, in Algebra.Algebra]
algebra_on_def [projection, in Algebra.Algebra]
algebra_carrier [projection, in Algebra.Algebra]
algebra_bilinear_map [projection, in Algebra.Algebra]
algebra_on [record, in Algebra.Algebra]
algebra_def.R [variable, in Algebra.Algebra]
algebra_def [section, in Algebra.Algebra]
Algebra_facts [library]
Ap [projection, in Algebra.Sets]
app_rel [definition, in Algebra.Sets]
Ap_comp [lemma, in Algebra.Sets]
asg [definition, in Algebra.Group_util]
asg [definition, in Algebra.Monoid_util]
associative [definition, in Algebra.Sgroup_cat]
ax1 [lemma, in Algebra.Z_group]
ax2 [lemma, in Algebra.Z_group]
ax3 [lemma, in Algebra.Z_group]
ax4 [lemma, in Algebra.Z_group]
ax5 [lemma, in Algebra.Z_group]
ax6 [lemma, in Algebra.Z_group]
ax7 [lemma, in Algebra.Z_group]
ax8 [lemma, in Algebra.Z_group]
B
bijective [definition, in Algebra.Sets]bijective_surjective [lemma, in Algebra.Sets]
bijective_injective [lemma, in Algebra.Sets]
bijective_comp [lemma, in Algebra.Sets]
bij_group_quo_ker_coKer_bijective [lemma, in Algebra.Group_hom_factor]
bij_group_quo_ker_coKer [definition, in Algebra.Group_hom_factor]
BUILD_SUB_GROUP [definition, in Algebra.Group_util]
Build_sub_group.Hinv [variable, in Algebra.Group_util]
Build_sub_group.Hunit [variable, in Algebra.Group_util]
Build_sub_group.Hlaw [variable, in Algebra.Group_util]
Build_sub_group.H [variable, in Algebra.Group_util]
Build_sub_group.G [variable, in Algebra.Group_util]
Build_sub_group [section, in Algebra.Group_util]
BUILD_HOM_GROUP [definition, in Algebra.Group_util]
BUILD_ABELIAN_GROUP [definition, in Algebra.Group_util]
BUILD_GROUP [definition, in Algebra.Group_util]
Build_Ctype_comp2 [lemma, in Algebra.Complex_field]
Build_Ctype_comp [lemma, in Algebra.Complex_field]
BUILD_MODULE_GROUP [definition, in Algebra.Module_util]
BUILD_HOM_MODULE [definition, in Algebra.Module_util]
BUILD_MODULE [definition, in Algebra.Module_util]
BUILD_SUB_MONOID [definition, in Algebra.Monoid_util]
Build_sub_monoid.Hunit [variable, in Algebra.Monoid_util]
Build_sub_monoid.Hlaw [variable, in Algebra.Monoid_util]
Build_sub_monoid.H [variable, in Algebra.Monoid_util]
Build_sub_monoid.G [variable, in Algebra.Monoid_util]
Build_sub_monoid [section, in Algebra.Monoid_util]
BUILD_HOM_MONOID [definition, in Algebra.Monoid_util]
BUILD_ABELIAN_MONOID [definition, in Algebra.Monoid_util]
BUILD_MONOID [definition, in Algebra.Monoid_util]
BUILD_HOM_RING [definition, in Algebra.Ring_util]
BUILD_RING [definition, in Algebra.Ring_util]
C
Cadd [definition, in Algebra.Complex_field]Cantor_Berstein [lemma, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.map_extend [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.partial_section [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.img [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.PXeq [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.hXX [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.XhX [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.X [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.PX [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.h_incr [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.h [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.ginj [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.finj [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.g [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.f [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.F [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein.E [variable, in Algebra.Cantor_Bernstein]
Cantor_Bernstein [section, in Algebra.Cantor_Bernstein]
Cantor_Bernstein [library]
cardinal [inductive, in Algebra.Fpart]
cardinalO_unique [lemma, in Algebra.Fpart]
cardinal_minus_part [lemma, in Algebra.Tiroirs]
cardinal_union_inter [lemma, in Algebra.Fpart2]
cardinal_diff [lemma, in Algebra.Fpart2]
cardinal_union [lemma, in Algebra.Fpart2]
cardinal_union_disjoint [lemma, in Algebra.Fpart2]
cardinal_unique [lemma, in Algebra.Fpart]
cardinal_S [lemma, in Algebra.Fpart]
cardinal_ind2 [lemma, in Algebra.Fpart]
cardinal_sup3 [lemma, in Algebra.Fpart]
cardinal_1_single [lemma, in Algebra.Fpart]
cardinal_O_empty [lemma, in Algebra.Fpart]
cardinal_pair [lemma, in Algebra.Fpart]
cardinal_single [lemma, in Algebra.Fpart]
cardinal_empty_O [lemma, in Algebra.Fpart]
cardinal_comp_r [lemma, in Algebra.Fpart]
cardinal_comp_l [lemma, in Algebra.Fpart]
cardinal_comp [lemma, in Algebra.Fpart]
cardinal_add [constructor, in Algebra.Fpart]
cardinal_empty [constructor, in Algebra.Fpart]
cardinal_included [lemma, in Algebra.Fmap]
cardinal_equal_included_equal [axiom, in Algebra.Fmap]
cardinal_image_equal_injective [lemma, in Algebra.Fmap]
cardinal_image_strict_lesser [lemma, in Algebra.Fmap]
cardinal_image_injective [lemma, in Algebra.Fmap]
cardinal_image_lesser [lemma, in Algebra.Fmap]
Carrier [projection, in Algebra.Sets]
cart [definition, in Algebra.Cartesian]
Cartesian [library]
cart_eq_equiv [lemma, in Algebra.Cartesian]
cart_eq [definition, in Algebra.Cartesian]
cart_r [projection, in Algebra.Cartesian]
cart_l [projection, in Algebra.Cartesian]
cart_type [record, in Algebra.Cartesian]
Categories [library]
Categories2 [library]
category [record, in Algebra.Categories]
Category_def.Full_subcat_def.i [variable, in Algebra.Categories]
Category_def.Full_subcat_def.C' [variable, in Algebra.Categories]
Category_def.Full_subcat_def.C [variable, in Algebra.Categories]
Category_def.Full_subcat_def [section, in Algebra.Categories]
Category_def.Category_comp.C [variable, in Algebra.Categories]
Category_def.Category_comp [section, in Algebra.Categories]
Category_def.Category_def1.Hom_id [variable, in Algebra.Categories]
Category_def.Category_def1.Hom_comp [variable, in Algebra.Categories]
Category_def.Category_def1.Hom [variable, in Algebra.Categories]
Category_def.Category_def1.Ob [variable, in Algebra.Categories]
Category_def.Category_def1 [section, in Algebra.Categories]
Category_def [section, in Algebra.Categories]
CC [definition, in Algebra.Complex_field]
Ccring [definition, in Algebra.Complex_field]
Cdistrib_prf [projection, in Algebra.Categories2]
CdivR [definition, in Algebra.Complex_field]
Ceq [definition, in Algebra.Complex_field]
Cfctr_morph [projection, in Algebra.Categories2]
Cfctr_ob [projection, in Algebra.Categories2]
CFIELD [definition, in Algebra.Cfield_cat]
cfield [record, in Algebra.Cfield_cat]
cfield_on_def [projection, in Algebra.Cfield_cat]
cfield_ring [projection, in Algebra.Cfield_cat]
CFIELD_mult_div_r [lemma, in Algebra.Cfield_facts]
CFIELD_mult3bis [lemma, in Algebra.Cfield_facts]
CFIELD_mult3 [lemma, in Algebra.Cfield_facts]
CFIELD_mult4 [lemma, in Algebra.Cfield_facts]
CFIELD_simpl_l [lemma, in Algebra.Cfield_facts]
CFIELD_inverse_law2 [lemma, in Algebra.Cfield_facts]
CFIELD_com [lemma, in Algebra.Cfield_facts]
Cfield_cat [library]
Cfield_facts [library]
Cfunctor [record, in Algebra.Categories2]
Cim_of_id_prf [projection, in Algebra.Categories2]
Cinv [definition, in Algebra.Complex_field]
Cinv_map [definition, in Algebra.Complex_field]
Cmult [definition, in Algebra.Complex_field]
coKer [definition, in Algebra.Group_kernel]
coKer [definition, in Algebra.Module_kernel]
coKer_prop [lemma, in Algebra.Group_kernel]
coKer_prop [lemma, in Algebra.Module_kernel]
commutative [definition, in Algebra.Abelian_group_cat]
Commutative_rings.R1 [variable, in Algebra.Ring_facts]
Commutative_rings [section, in Algebra.Ring_facts]
compl [definition, in Algebra.Parts2]
Complement1 [section, in Algebra.Parts2]
Complement1.E [variable, in Algebra.Parts2]
Complex_field [library]
compl_not_compl [lemma, in Algebra.Parts2]
compl_included [lemma, in Algebra.Parts2]
compl_not_in [lemma, in Algebra.Parts2]
compl_compl [lemma, in Algebra.Parts2]
compl_comp_rev [lemma, in Algebra.Parts2]
compl_comp [lemma, in Algebra.Parts2]
compl_in [lemma, in Algebra.Parts2]
comp_hom_unit_r [lemma, in Algebra.Categories]
comp_hom_unit_l [lemma, in Algebra.Categories]
comp_hom_assoc [lemma, in Algebra.Categories]
comp_hom_compatible [lemma, in Algebra.Categories]
comp_hom [definition, in Algebra.Categories]
comp_is_id_then_surjective [lemma, in Algebra.Sets]
comp_is_id_then_injective [lemma, in Algebra.Sets]
comp_is_id_then_bijective [lemma, in Algebra.Sets]
comp_surjective [lemma, in Algebra.Sets]
comp_injective [lemma, in Algebra.Sets]
comp_map_assoc [lemma, in Algebra.Sets]
comp_map_comp [lemma, in Algebra.Sets]
comp_map_map [definition, in Algebra.Sets]
comp_map_fun_compatible [lemma, in Algebra.Sets]
comp_map_fun [definition, in Algebra.Sets]
comp_map_map_compatible [lemma, in Algebra.Set_cat]
Cone [definition, in Algebra.Complex_field]
conjugate [definition, in Algebra.Complex_field]
Copp [definition, in Algebra.Complex_field]
couple [definition, in Algebra.Cartesian]
couple_comp [lemma, in Algebra.Cartesian]
coupl_proj [lemma, in Algebra.Cartesian]
Cring [definition, in Algebra.Complex_field]
CRING [definition, in Algebra.Ring_cat]
cring [record, in Algebra.Ring_cat]
cring_monoid [definition, in Algebra.Ring_cat]
cring_on_def [projection, in Algebra.Ring_cat]
cring_ring [projection, in Algebra.Ring_cat]
cring_com_prf [projection, in Algebra.Ring_cat]
cring_on [record, in Algebra.Ring_cat]
CRING_mult3bis [lemma, in Algebra.Ring_facts]
CRING_mult3 [lemma, in Algebra.Ring_facts]
CRING_mult4 [lemma, in Algebra.Ring_facts]
CRING_com [lemma, in Algebra.Ring_facts]
Cset [definition, in Algebra.Complex_field]
Ctype [record, in Algebra.Complex_field]
curry [definition, in Algebra.Cartesian]
Czero [definition, in Algebra.Complex_field]
C_field_on [definition, in Algebra.Complex_field]
C_inv_r [lemma, in Algebra.Complex_field]
D
Def [section, in Algebra.Module_cat]Def [section, in Algebra.Complex_field]
Def [section, in Algebra.Sub_module]
Def [section, in Algebra.Sub_group]
Def [section, in Algebra.Group_kernel]
Def [section, in Algebra.Group_quotient]
Def [section, in Algebra.Endo_set]
Def [section, in Algebra.Group_of_group_hom]
Def [section, in Algebra.Operation_of_monoid]
Def [section, in Algebra.Fraction_field]
Def [section, in Algebra.Group_hom_factor]
Def [section, in Algebra.Sub_sgroup]
Def [section, in Algebra.Set_cat]
Def [section, in Algebra.Cartesian]
Def [section, in Algebra.Sub_monoid]
Def [section, in Algebra.Module_kernel]
Def.diff10 [variable, in Algebra.Fraction_field]
Def.E [variable, in Algebra.Endo_set]
Def.E [variable, in Algebra.Cartesian]
Def.f [variable, in Algebra.Group_kernel]
Def.f [variable, in Algebra.Group_hom_factor]
Def.F [variable, in Algebra.Cartesian]
Def.f [variable, in Algebra.Module_kernel]
Def.ff_field_on [variable, in Algebra.Fraction_field]
Def.ff_inr_r [variable, in Algebra.Fraction_field]
Def.G [variable, in Algebra.Sub_group]
Def.G [variable, in Algebra.Group_kernel]
Def.G [variable, in Algebra.Group_quotient]
Def.G [variable, in Algebra.Group_of_group_hom]
Def.G [variable, in Algebra.Group_hom_factor]
Def.G [variable, in Algebra.Sub_sgroup]
Def.G [variable, in Algebra.Sub_monoid]
Def.G' [variable, in Algebra.Group_kernel]
Def.G' [variable, in Algebra.Group_of_group_hom]
Def.G' [variable, in Algebra.Group_hom_factor]
Def.H [variable, in Algebra.Group_quotient]
Def.Hnormal [variable, in Algebra.Group_quotient]
Def.Hom [section, in Algebra.Module_cat]
Def.Hom.E [variable, in Algebra.Module_cat]
Def.Hom.F [variable, in Algebra.Module_cat]
Def.M [variable, in Algebra.Sub_module]
Def.M [variable, in Algebra.Operation_of_monoid]
Def.Mod [variable, in Algebra.Module_kernel]
Def.Module_def.op [variable, in Algebra.Module_cat]
Def.Module_def.Mod [variable, in Algebra.Module_cat]
Def.Module_def [section, in Algebra.Module_cat]
Def.Mod2 [variable, in Algebra.Module_kernel]
Def.op [variable, in Algebra.Operation_of_monoid]
Def.R [variable, in Algebra.Module_cat]
Def.R [variable, in Algebra.Complex_field]
Def.R [variable, in Algebra.Sub_module]
Def.R [variable, in Algebra.Fraction_field]
Def.R [variable, in Algebra.Module_kernel]
Def.S [variable, in Algebra.Operation_of_monoid]
Def.Sub_module.endofun [variable, in Algebra.Sub_module]
Def.Sub_module.Na [variable, in Algebra.Sub_module]
Def.Sub_module.Nop [variable, in Algebra.Sub_module]
Def.Sub_module.N [variable, in Algebra.Sub_module]
Def.Sub_module [section, in Algebra.Sub_module]
Def.Sub_group.Hinv [variable, in Algebra.Sub_group]
Def.Sub_group.H [variable, in Algebra.Sub_group]
Def.Sub_group [section, in Algebra.Sub_group]
Def.Sub_sgroup.Hprop [variable, in Algebra.Sub_sgroup]
Def.Sub_sgroup.H [variable, in Algebra.Sub_sgroup]
Def.Sub_sgroup [section, in Algebra.Sub_sgroup]
Def.Sub_monoid.Hunit [variable, in Algebra.Sub_monoid]
Def.Sub_monoid.H [variable, in Algebra.Sub_monoid]
Def.Sub_monoid [section, in Algebra.Sub_monoid]
Def.sum_of_square [variable, in Algebra.Complex_field]
Def.zero_dec [variable, in Algebra.Fraction_field]
den [projection, in Algebra.Fraction_field]
den_prf [projection, in Algebra.Fraction_field]
diff [definition, in Algebra.Diff]
Diff [section, in Algebra.Diff]
Diff [library]
diff_comp [lemma, in Algebra.Diff]
diff_add_part2 [lemma, in Algebra.Tiroirs]
diff_add_part_not_in [lemma, in Algebra.Fpart2]
diff_not_in [lemma, in Algebra.Fpart2]
diff_add_part [lemma, in Algebra.Fpart2]
diff_in_r [lemma, in Algebra.Fpart2]
diff_in_l [lemma, in Algebra.Fpart2]
diff_el_union_single [axiom, in Algebra.Fmap]
diff_single_not_in [axiom, in Algebra.Fmap]
Diff.E [variable, in Algebra.Diff]
disjoint [definition, in Algebra.Fpart2]
disjoint_diff [lemma, in Algebra.Fpart2]
disjoint_not_in_r [lemma, in Algebra.Fpart2]
disjoint_inclus [lemma, in Algebra.Fpart2]
disjoint_comp [lemma, in Algebra.Fpart2]
distrib_prf [projection, in Algebra.Categories2]
dist_l [definition, in Algebra.Ring_cat]
dist_r [definition, in Algebra.Ring_cat]
E
empty [definition, in Algebra.Parts]empty_included [lemma, in Algebra.Parts]
empty_prop [lemma, in Algebra.Parts]
empty_inter [lemma, in Algebra.Fpart2]
empty_diff [lemma, in Algebra.Fpart2]
empty_not_in [lemma, in Algebra.Fpart2]
Endo_SET [definition, in Algebra.Endo_set]
Endo_SET_sgroup [definition, in Algebra.Endo_set]
endo_comp [definition, in Algebra.Endo_set]
Endo_set [library]
eqFaG [inductive, in Algebra.Free_abelian_group]
eqFaG_Equiv [lemma, in Algebra.Free_abelian_group]
eqFaG_com [constructor, in Algebra.Free_abelian_group]
eqFaG_trans [constructor, in Algebra.Free_abelian_group]
eqFaG_sym [constructor, in Algebra.Free_abelian_group]
eqFaG_refl [constructor, in Algebra.Free_abelian_group]
eqFaG_invr [constructor, in Algebra.Free_abelian_group]
eqFaG_inv [constructor, in Algebra.Free_abelian_group]
eqFaG_law0r [constructor, in Algebra.Free_abelian_group]
eqFaG_law_assoc [constructor, in Algebra.Free_abelian_group]
eqFaG_law [constructor, in Algebra.Free_abelian_group]
eqFaG_Var [constructor, in Algebra.Free_abelian_group]
eqFaM [inductive, in Algebra.Free_abelian_monoid]
eqFaM_Equiv [lemma, in Algebra.Free_abelian_monoid]
eqFaM_com [constructor, in Algebra.Free_abelian_monoid]
eqFaM_trans [constructor, in Algebra.Free_abelian_monoid]
eqFaM_sym [constructor, in Algebra.Free_abelian_monoid]
eqFaM_refl [constructor, in Algebra.Free_abelian_monoid]
eqFaM_law0l [constructor, in Algebra.Free_abelian_monoid]
eqFaM_law0r [constructor, in Algebra.Free_abelian_monoid]
eqFaM_law_assoc [constructor, in Algebra.Free_abelian_monoid]
eqFaM_law [constructor, in Algebra.Free_abelian_monoid]
eqFaM_Var [constructor, in Algebra.Free_abelian_monoid]
eqFG [inductive, in Algebra.Free_group]
eqFG_Equiv [lemma, in Algebra.Free_group]
eqFG_trans [constructor, in Algebra.Free_group]
eqFG_sym [constructor, in Algebra.Free_group]
eqFG_refl [constructor, in Algebra.Free_group]
eqFG_invr [constructor, in Algebra.Free_group]
eqFG_inv [constructor, in Algebra.Free_group]
eqFG_law0r [constructor, in Algebra.Free_group]
eqFG_law_assoc [constructor, in Algebra.Free_group]
eqFG_law [constructor, in Algebra.Free_group]
eqFG_Var [constructor, in Algebra.Free_group]
eqFM [inductive, in Algebra.Free_monoid]
eqFMd [inductive, in Algebra.Free_module]
eqFMd_Equiv [lemma, in Algebra.Free_module]
eqFMd_op_unit [constructor, in Algebra.Free_module]
eqFMd_op_assoc [constructor, in Algebra.Free_module]
eqFMd_oplin_r [constructor, in Algebra.Free_module]
eqFMd_oplin_l [constructor, in Algebra.Free_module]
eqFMd_op_comp [constructor, in Algebra.Free_module]
eqFMd_com [constructor, in Algebra.Free_module]
eqFMd_trans [constructor, in Algebra.Free_module]
eqFMd_sym [constructor, in Algebra.Free_module]
eqFMd_refl [constructor, in Algebra.Free_module]
eqFMd_invr [constructor, in Algebra.Free_module]
eqFMd_inv [constructor, in Algebra.Free_module]
eqFMd_law0r [constructor, in Algebra.Free_module]
eqFMd_law_assoc [constructor, in Algebra.Free_module]
eqFMd_law [constructor, in Algebra.Free_module]
eqFMd_Var [constructor, in Algebra.Free_module]
eqFM_Equiv [lemma, in Algebra.Free_monoid]
eqFM_trans [constructor, in Algebra.Free_monoid]
eqFM_sym [constructor, in Algebra.Free_monoid]
eqFM_refl [constructor, in Algebra.Free_monoid]
eqFM_law0l [constructor, in Algebra.Free_monoid]
eqFM_law0r [constructor, in Algebra.Free_monoid]
eqFM_law_assoc [constructor, in Algebra.Free_monoid]
eqFM_law [constructor, in Algebra.Free_monoid]
eqFM_Var [constructor, in Algebra.Free_monoid]
eqfraction [definition, in Algebra.Fraction_field]
eqfraction_trans [lemma, in Algebra.Fraction_field]
eqfraction_sym [lemma, in Algebra.Fraction_field]
eqfraction_num0 [lemma, in Algebra.Fraction_field]
eqfraction_refl [lemma, in Algebra.Fraction_field]
eqfraction0 [lemma, in Algebra.Fraction_field]
Equal [projection, in Algebra.Sets]
equivalence [definition, in Algebra.Sets]
equiv_trans [lemma, in Algebra.Sets]
equiv_sym [lemma, in Algebra.Sets]
equiv_refl [lemma, in Algebra.Sets]
eq_part_included [lemma, in Algebra.Parts]
eq_part [definition, in Algebra.Parts]
eunitgenlawl [lemma, in Algebra.Group_util]
eunitl [lemma, in Algebra.Group_util]
eunitl [lemma, in Algebra.Monoid_util]
eunitr [lemma, in Algebra.Group_util]
eunitr [lemma, in Algebra.Monoid_util]
F
f [definition, in Algebra.Group_util]f [definition, in Algebra.Monoid_util]
factor_group_hom [lemma, in Algebra.Group_hom_factor]
FaG [inductive, in Algebra.Free_abelian_group]
FaG_comp_prop [lemma, in Algebra.Free_abelian_group]
FaG_var [definition, in Algebra.Free_abelian_group]
FaG_lift [definition, in Algebra.Free_abelian_group]
FaG_lift_fun [definition, in Algebra.Free_abelian_group]
FaG_set [definition, in Algebra.Free_abelian_group]
FaM [inductive, in Algebra.Free_abelian_monoid]
FaM_comp_prop [lemma, in Algebra.Free_abelian_monoid]
FaM_var [definition, in Algebra.Free_abelian_monoid]
FaM_lift [definition, in Algebra.Free_abelian_monoid]
FaM_lift_fun [definition, in Algebra.Free_abelian_monoid]
FaM_set [definition, in Algebra.Free_abelian_monoid]
fassoc [lemma, in Algebra.Group_util]
fassoc [lemma, in Algebra.Monoid_util]
fctr_morph [projection, in Algebra.Categories2]
fctr_ob [projection, in Algebra.Categories2]
FG [inductive, in Algebra.Free_group]
FG_comp_prop [lemma, in Algebra.Free_group]
FG_var [definition, in Algebra.Free_group]
FG_lift [definition, in Algebra.Free_group]
FG_lift_fun [definition, in Algebra.Free_group]
FG_set [definition, in Algebra.Free_group]
fhomsg [definition, in Algebra.Group_util]
fhomsg [definition, in Algebra.Monoid_util]
FIELD [definition, in Algebra.Field_cat]
field [record, in Algebra.Field_cat]
field_on_def [projection, in Algebra.Field_cat]
field_ring [projection, in Algebra.Field_cat]
field_unit_non_zero [projection, in Algebra.Field_cat]
field_inverse_l_prf [projection, in Algebra.Field_cat]
field_inverse_r_prf [projection, in Algebra.Field_cat]
field_inverse_map [projection, in Algebra.Field_cat]
field_on [record, in Algebra.Field_cat]
FIELD_inv_div [lemma, in Algebra.Field_facts]
FIELD_div_div2 [lemma, in Algebra.Field_facts]
FIELD_mult_div_l [lemma, in Algebra.Field_facts]
FIELD_div_div [lemma, in Algebra.Field_facts]
FIELD_one_div_div [lemma, in Algebra.Field_facts]
FIELD_one_div_xy [lemma, in Algebra.Field_facts]
FIELD_one_div_x [lemma, in Algebra.Field_facts]
FIELD_simpl_r [lemma, in Algebra.Field_facts]
FIELD_x_div_x [lemma, in Algebra.Field_facts]
FIELD_inverse_law [lemma, in Algebra.Field_facts]
FIELD_law_inverse [lemma, in Algebra.Field_facts]
FIELD_integral_domain_r [lemma, in Algebra.Field_facts]
FIELD_integral_domain_l [lemma, in Algebra.Field_facts]
FIELD_inverse_inverse [lemma, in Algebra.Field_facts]
FIELD_inverse_non_zero [lemma, in Algebra.Field_facts]
FIELD_reg_right [lemma, in Algebra.Field_facts]
FIELD_reg_left [lemma, in Algebra.Field_facts]
FIELD_unit_inverse [lemma, in Algebra.Field_facts]
FIELD_comp [lemma, in Algebra.Field_facts]
FIELD_unit_non_zero [lemma, in Algebra.Field_facts]
FIELD_inverse_l [lemma, in Algebra.Field_facts]
FIELD_inverse_r [lemma, in Algebra.Field_facts]
field_div [definition, in Algebra.Field_facts]
field_inverse [definition, in Algebra.Field_facts]
Field_cat [library]
Field_facts [library]
finite [definition, in Algebra.Fmap]
finite_surjective_injective [lemma, in Algebra.Fmap]
finite_injective_surjective [lemma, in Algebra.Fmap]
FM [inductive, in Algebra.Free_monoid]
Fmap [library]
FMd [inductive, in Algebra.Free_module]
FMd_comp_prop [lemma, in Algebra.Free_module]
FMd_var [definition, in Algebra.Free_module]
FMd_lift [definition, in Algebra.Free_module]
FMd_lift_fun [definition, in Algebra.Free_module]
FMd_set [definition, in Algebra.Free_module]
FM_comp_prop [lemma, in Algebra.Free_monoid]
FM_var [definition, in Algebra.Free_monoid]
FM_lift [definition, in Algebra.Free_monoid]
FM_lift_fun [definition, in Algebra.Free_monoid]
FM_set [definition, in Algebra.Free_monoid]
Foncteurs [section, in Algebra.Categories2]
Foncteurs.Def_1.C2 [variable, in Algebra.Categories2]
Foncteurs.Def_1.C1 [variable, in Algebra.Categories2]
Foncteurs.Def_1 [section, in Algebra.Categories2]
Fpart [library]
fparts_in_def.E [variable, in Algebra.Fpart]
fparts_in_def [section, in Algebra.Fpart]
fparts2_def.E [variable, in Algebra.Fpart2]
fparts2_def [section, in Algebra.Fpart2]
Fpart2 [library]
fraction [record, in Algebra.Fraction_field]
fraction_cfield [definition, in Algebra.Fraction_field]
fraction_set [definition, in Algebra.Fraction_field]
Fraction_field [library]
fraction0 [definition, in Algebra.Fraction_field]
fraction1 [definition, in Algebra.Fraction_field]
fract_field_ring [definition, in Algebra.Fraction_field]
fract_field_ring_aux [definition, in Algebra.Fraction_field]
FreeAbelianGroup [definition, in Algebra.Free_abelian_group]
FreeAbelianMonoid [definition, in Algebra.Free_abelian_monoid]
FreeGroup [definition, in Algebra.Free_group]
FreeModule [definition, in Algebra.Free_module]
FreeMonoid [definition, in Algebra.Free_monoid]
Free_monoid_def.Universal_prop.f [variable, in Algebra.Free_monoid]
Free_monoid_def.Universal_prop.M [variable, in Algebra.Free_monoid]
Free_monoid_def.Universal_prop [section, in Algebra.Free_monoid]
Free_monoid_def.V [variable, in Algebra.Free_monoid]
Free_monoid_def [section, in Algebra.Free_monoid]
Free_group_def.Universal_prop.f [variable, in Algebra.Free_group]
Free_group_def.Universal_prop.G [variable, in Algebra.Free_group]
Free_group_def.Universal_prop [section, in Algebra.Free_group]
Free_group_def.V [variable, in Algebra.Free_group]
Free_group_def [section, in Algebra.Free_group]
Free_abelian_monoid_def.Universal_prop.f [variable, in Algebra.Free_abelian_monoid]
Free_abelian_monoid_def.Universal_prop.M [variable, in Algebra.Free_abelian_monoid]
Free_abelian_monoid_def.Universal_prop [section, in Algebra.Free_abelian_monoid]
Free_abelian_monoid_def.V [variable, in Algebra.Free_abelian_monoid]
Free_abelian_monoid_def [section, in Algebra.Free_abelian_monoid]
Free_Module_def.Universal_prop.f [variable, in Algebra.Free_module]
Free_Module_def.Universal_prop.Mod [variable, in Algebra.Free_module]
Free_Module_def.Universal_prop [section, in Algebra.Free_module]
Free_Module_def.V [variable, in Algebra.Free_module]
Free_Module_def.R [variable, in Algebra.Free_module]
Free_Module_def [section, in Algebra.Free_module]
Free_abelian_group_def.Universal_prop.f [variable, in Algebra.Free_abelian_group]
Free_abelian_group_def.Universal_prop.G [variable, in Algebra.Free_abelian_group]
Free_abelian_group_def.Universal_prop [section, in Algebra.Free_abelian_group]
Free_abelian_group_def.V [variable, in Algebra.Free_abelian_group]
Free_abelian_group_def [section, in Algebra.Free_abelian_group]
Free_group [library]
Free_abelian_group [library]
Free_monoid [library]
Free_module [library]
Free_abelian_monoid [library]
fsubcat_Hom_id [definition, in Algebra.Categories]
fsubcat_Hom_comp [definition, in Algebra.Categories]
fsubcat_Hom [definition, in Algebra.Categories]
full [definition, in Algebra.Parts]
full_subcat [definition, in Algebra.Categories]
full_included [lemma, in Algebra.Parts]
full_set_full [lemma, in Algebra.Parts]
full_to_set [definition, in Algebra.Parts]
full_prop [lemma, in Algebra.Parts]
functor [record, in Algebra.Categories2]
fun_compatible [definition, in Algebra.Sets]
fun2_compatible [definition, in Algebra.Cartesian]
f2 [definition, in Algebra.Group_util]
f2 [definition, in Algebra.Monoid_util]
G
G [definition, in Algebra.Group_util]G [definition, in Algebra.Ring_util]
generated_monoid_prop_rev [lemma, in Algebra.Generated_monoid]
generated_monoid_prop [lemma, in Algebra.Generated_monoid]
generated_monoid_prop_included [lemma, in Algebra.Generated_monoid]
generated_monoid_minimal [lemma, in Algebra.Generated_monoid]
generated_monoid [definition, in Algebra.Generated_monoid]
Generated_monoid_def.A [variable, in Algebra.Generated_monoid]
Generated_monoid_def.M [variable, in Algebra.Generated_monoid]
Generated_monoid_def [section, in Algebra.Generated_monoid]
generated_group_prop_rev [lemma, in Algebra.Generated_group]
generated_group_prop [lemma, in Algebra.Generated_group]
generated_group_prop_included [lemma, in Algebra.Generated_group]
generated_group_minimal [lemma, in Algebra.Generated_group]
generated_group [definition, in Algebra.Generated_group]
Generated_group_def.A [variable, in Algebra.Generated_group]
Generated_group_def.G [variable, in Algebra.Generated_group]
Generated_group_def [section, in Algebra.Generated_group]
generated_ideal_minimal [lemma, in Algebra.Ideal]
generated_ideal_included [lemma, in Algebra.Ideal]
generated_ideal [definition, in Algebra.Ideal]
generated_module_subgroup [definition, in Algebra.Ideal]
Generated_ideal.A [variable, in Algebra.Ideal]
Generated_ideal.R [variable, in Algebra.Ideal]
Generated_ideal [section, in Algebra.Ideal]
generated_module_prop_rev [lemma, in Algebra.Generated_module]
generated_module_prop [lemma, in Algebra.Generated_module]
generated_module_prop_included [lemma, in Algebra.Generated_module]
generated_module_minimal [lemma, in Algebra.Generated_module]
generated_module [definition, in Algebra.Generated_module]
Generated_module_def.A [variable, in Algebra.Generated_module]
Generated_module_def.Mod [variable, in Algebra.Generated_module]
Generated_module_def.R [variable, in Algebra.Generated_module]
Generated_module_def [section, in Algebra.Generated_module]
Generated_module [library]
Generated_group [library]
Generated_monoid [library]
geninvl [lemma, in Algebra.Group_util]
Group [section, in Algebra.Group_util]
GROUP [definition, in Algebra.Group_cat]
group [record, in Algebra.Group_cat]
Group [section, in Algebra.Abelian_group_facts]
GROUP_hom_prop [lemma, in Algebra.Group_facts]
GROUP_inverse_law [lemma, in Algebra.Group_facts]
GROUP_law_inverse [lemma, in Algebra.Group_facts]
GROUP_inverse_inverse [lemma, in Algebra.Group_facts]
GROUP_reg_right [lemma, in Algebra.Group_facts]
GROUP_reg_left [lemma, in Algebra.Group_facts]
GROUP_unit_inverse [lemma, in Algebra.Group_facts]
GROUP_inverse_l [lemma, in Algebra.Group_facts]
GROUP_inverse_r [lemma, in Algebra.Group_facts]
GROUP_comp [lemma, in Algebra.Group_facts]
group_of_subgroup [definition, in Algebra.Sub_group]
group_quo_ker [definition, in Algebra.Group_kernel]
group_power_mult [lemma, in Algebra.Z_group_facts]
group_power_inv [lemma, in Algebra.Z_group_facts]
group_power_1 [lemma, in Algebra.Z_group_facts]
group_power_0 [lemma, in Algebra.Z_group_facts]
group_power_S [lemma, in Algebra.Z_group_facts]
group_power_plus [lemma, in Algebra.Z_group_facts]
group_quo_surj [definition, in Algebra.Group_quotient]
group_quo [definition, in Algebra.Group_quotient]
group_quo_set [definition, in Algebra.Group_quotient]
group_quo_eqrel_equiv [lemma, in Algebra.Group_quotient]
group_quo_eqrel [definition, in Algebra.Group_quotient]
group_quo_eq [definition, in Algebra.Group_quotient]
group_hom_inv_prop [lemma, in Algebra.Group_of_group_hom]
group_hom_unit_prop [lemma, in Algebra.Group_of_group_hom]
group_hom_law_prop [lemma, in Algebra.Group_of_group_hom]
group_hom [definition, in Algebra.Group_of_group_hom]
group_hom_inv [definition, in Algebra.Group_of_group_hom]
group_hom_unit [definition, in Algebra.Group_of_group_hom]
group_hom_law [definition, in Algebra.Group_of_group_hom]
group_inverse [definition, in Algebra.Group_cat]
group_on_def [projection, in Algebra.Group_cat]
group_monoid [projection, in Algebra.Group_cat]
group_inverse_l_prf [projection, in Algebra.Group_cat]
group_inverse_r_prf [projection, in Algebra.Group_cat]
group_inverse_map [projection, in Algebra.Group_cat]
group_on [record, in Algebra.Group_cat]
group_power [definition, in Algebra.Z_group]
group_square [definition, in Algebra.Z_group]
group_power_S [axiom, in Algebra.Group_power]
group_power_zero [lemma, in Algebra.Group_power]
group_power [definition, in Algebra.Group_power]
group_power_pos [definition, in Algebra.Group_power]
group_square [definition, in Algebra.Group_power]
Group_hom_factor [library]
Group_of_group_hom [library]
Group_kernel [library]
Group_power [library]
Group_cat [library]
Group_facts [library]
Group_util [library]
Group_quotient [library]
Group.e [variable, in Algebra.Group_util]
Group.E [variable, in Algebra.Group_util]
Group.eunitgenlawr [variable, in Algebra.Group_util]
Group.fcomp [variable, in Algebra.Group_util]
Group.G [variable, in Algebra.Abelian_group_facts]
Group.geninv [variable, in Algebra.Group_util]
Group.geninvr [variable, in Algebra.Group_util]
Group.genlaw [variable, in Algebra.Group_util]
Group.genlawassoc [variable, in Algebra.Group_util]
Group.invcomp [variable, in Algebra.Group_util]
H
Hom [section, in Algebra.Group_util]Hom [projection, in Algebra.Categories]
Hom [section, in Algebra.Ring_cat]
Hom [section, in Algebra.Monoid_cat]
Hom [section, in Algebra.Sgroup_cat]
Hom [section, in Algebra.Module_util]
Hom [section, in Algebra.Monoid_util]
Hom [section, in Algebra.Ring_util]
Hom_module [definition, in Algebra.Hom_module]
Hom_module_def.Mod2 [variable, in Algebra.Hom_module]
Hom_module_def.Mod1 [variable, in Algebra.Hom_module]
Hom_module_def.R [variable, in Algebra.Hom_module]
Hom_module_def [section, in Algebra.Hom_module]
Hom_comp_unit_r_prf [projection, in Algebra.Categories]
Hom_comp_unit_l_prf [projection, in Algebra.Categories]
Hom_comp_assoc_prf [projection, in Algebra.Categories]
Hom_id [projection, in Algebra.Categories]
Hom_comp [projection, in Algebra.Categories]
Hom_comp_unit_r [definition, in Algebra.Categories]
Hom_comp_unit_l [definition, in Algebra.Categories]
Hom_comp_assoc [definition, in Algebra.Categories]
Hom_lemmas.f [variable, in Algebra.Ring_facts]
Hom_lemmas.R' [variable, in Algebra.Ring_facts]
Hom_lemmas.R [variable, in Algebra.Ring_facts]
Hom_lemmas [section, in Algebra.Ring_facts]
Hom_module [library]
Hom.E [variable, in Algebra.Ring_cat]
Hom.E [variable, in Algebra.Monoid_cat]
Hom.E [variable, in Algebra.Sgroup_cat]
Hom.F [variable, in Algebra.Ring_cat]
Hom.F [variable, in Algebra.Monoid_cat]
Hom.F [variable, in Algebra.Sgroup_cat]
Hom.ff [variable, in Algebra.Group_util]
Hom.ff [variable, in Algebra.Module_util]
Hom.ff [variable, in Algebra.Monoid_util]
Hom.ff [variable, in Algebra.Ring_util]
Hom.ffcomp [variable, in Algebra.Group_util]
Hom.ffcomp [variable, in Algebra.Module_util]
Hom.ffcomp [variable, in Algebra.Monoid_util]
Hom.ffcomp [variable, in Algebra.Ring_util]
Hom.fflaw [variable, in Algebra.Group_util]
Hom.fflaw [variable, in Algebra.Module_util]
Hom.fflaw [variable, in Algebra.Monoid_util]
Hom.ffmult [variable, in Algebra.Ring_util]
Hom.ffone [variable, in Algebra.Ring_util]
Hom.ffop [variable, in Algebra.Module_util]
Hom.ffplus [variable, in Algebra.Ring_util]
Hom.ffunit [variable, in Algebra.Group_util]
Hom.ffunit [variable, in Algebra.Module_util]
Hom.ffunit [variable, in Algebra.Monoid_util]
Hom.ffzero [variable, in Algebra.Ring_util]
Hom.G [variable, in Algebra.Group_util]
Hom.G [variable, in Algebra.Monoid_util]
Hom.G' [variable, in Algebra.Group_util]
Hom.G' [variable, in Algebra.Monoid_util]
Hom.Mod [variable, in Algebra.Module_util]
Hom.Mod' [variable, in Algebra.Module_util]
Hom.R [variable, in Algebra.Module_util]
Hom.Ring1 [variable, in Algebra.Ring_util]
Hom.Ring2 [variable, in Algebra.Ring_util]
I
Id [definition, in Algebra.Sets]ideal [record, in Algebra.Ideal]
Ideal [library]
ideals [section, in Algebra.Ideal]
ideals.R [variable, in Algebra.Ideal]
ideal_prop4 [lemma, in Algebra.Ideal]
ideal_prop3 [lemma, in Algebra.Ideal]
ideal_prop2 [lemma, in Algebra.Ideal]
ideal_prop [lemma, in Algebra.Ideal]
ideal_prf [projection, in Algebra.Ideal]
ideal_subgroup [projection, in Algebra.Ideal]
idomain [record, in Algebra.Integral_domain_cat]
idomain_on_def [projection, in Algebra.Integral_domain_cat]
idomain_ring [projection, in Algebra.Integral_domain_cat]
idomain_prf [projection, in Algebra.Integral_domain_cat]
idomain_on [record, in Algebra.Integral_domain_cat]
idomain_prop [definition, in Algebra.Integral_domain_cat]
Id_is_bijective [lemma, in Algebra.Sets]
Id_unit_l [lemma, in Algebra.Sets]
Id_unit_r [lemma, in Algebra.Sets]
id_map_parts_equal_prop [lemma, in Algebra.Parts]
id_map_parts_equal [definition, in Algebra.Parts]
imag [projection, in Algebra.Complex_field]
image [definition, in Algebra.Parts2]
Images1 [section, in Algebra.Parts2]
Images1.E [variable, in Algebra.Parts2]
Images1.f [variable, in Algebra.Parts2]
Images1.F [variable, in Algebra.Parts2]
Images1.surj_part_image_fun [variable, in Algebra.Parts2]
Images1.surj_set_image_fun [variable, in Algebra.Parts2]
image_map [definition, in Algebra.Parts2]
image_in_image [lemma, in Algebra.Parts2]
image_comp [lemma, in Algebra.Parts2]
image_included [lemma, in Algebra.Parts2]
image_in [lemma, in Algebra.Parts2]
image_invimage_image [lemma, in Algebra.Parts3]
image_invimage [lemma, in Algebra.Parts3]
image_monoid_prop_rev [lemma, in Algebra.Monoid_kernel]
image_monoid_prop [lemma, in Algebra.Monoid_kernel]
image_monoid_hom [definition, in Algebra.Monoid_kernel]
Image_hom.f [variable, in Algebra.Monoid_kernel]
Image_hom.M' [variable, in Algebra.Monoid_kernel]
Image_hom.M [variable, in Algebra.Monoid_kernel]
Image_hom [section, in Algebra.Monoid_kernel]
image_full_surjective [axiom, in Algebra.Fmap]
image_single [axiom, in Algebra.Fmap]
image_union [axiom, in Algebra.Fmap]
image_empty [axiom, in Algebra.Fmap]
imag_comp [lemma, in Algebra.Complex_field]
im_of_id_prf [projection, in Algebra.Categories2]
included [definition, in Algebra.Parts]
included_comp [lemma, in Algebra.Parts]
included_trans [lemma, in Algebra.Parts]
included_antisym [lemma, in Algebra.Parts]
included_refl [lemma, in Algebra.Parts]
included_inter_r [lemma, in Algebra.Inter]
included_inter_l [lemma, in Algebra.Inter]
included_add_part [lemma, in Algebra.Fpart2]
included_union_r [lemma, in Algebra.Union]
included_union_l [lemma, in Algebra.Union]
included2_inter [lemma, in Algebra.Inter]
included2_union [lemma, in Algebra.Union]
Inclusion [section, in Algebra.Parts]
Inclusion.E [variable, in Algebra.Parts]
Injection [section, in Algebra.Sub_module]
Injection [section, in Algebra.Sub_group]
Injection [section, in Algebra.Sub_sgroup]
Injection [section, in Algebra.Sub_monoid]
Injection.G [variable, in Algebra.Sub_group]
Injection.G [variable, in Algebra.Sub_sgroup]
Injection.G [variable, in Algebra.Sub_monoid]
Injection.H [variable, in Algebra.Sub_group]
Injection.H [variable, in Algebra.Sub_sgroup]
Injection.H [variable, in Algebra.Sub_monoid]
Injection.M [variable, in Algebra.Sub_module]
Injection.N [variable, in Algebra.Sub_module]
Injection.R [variable, in Algebra.Sub_module]
injective [definition, in Algebra.Sets]
injective_comp [lemma, in Algebra.Sets]
inj_submodule_injective [lemma, in Algebra.Sub_module]
inj_submodule [definition, in Algebra.Sub_module]
inj_subgroup_injective [lemma, in Algebra.Sub_group]
inj_subgroup [definition, in Algebra.Sub_group]
inj_part_included_injective [lemma, in Algebra.Parts]
inj_part_included_prop [lemma, in Algebra.Parts]
inj_part_included [definition, in Algebra.Parts]
inj_part_injective [lemma, in Algebra.Parts]
inj_part [definition, in Algebra.Parts]
inj_coKer_group_injective [lemma, in Algebra.Group_hom_factor]
inj_coKer_group [definition, in Algebra.Group_hom_factor]
inj_subgroup_injective [lemma, in Algebra.Sub_sgroup]
inj_subsgroup [definition, in Algebra.Sub_sgroup]
inj_subsmonoid_injective [lemma, in Algebra.Sub_monoid]
inj_submonoid [definition, in Algebra.Sub_monoid]
INTEGRAL_DOMAIN [definition, in Algebra.Integral_domain_cat]
INTEGRAL_DOMAIN_mult_eq_l [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_eq_r [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_simpl_l [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_simpl_r [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_n0_l [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_n0_r [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_r [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_l [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_prop [lemma, in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_prop_rev [lemma, in Algebra.Integral_domain_facts]
Integral_domain_cat [library]
Integral_domain_facts [library]
inter [definition, in Algebra.Inter]
Inter [library]
inter_union_dist_l [axiom, in Algebra.Inter]
inter_union_dist_r [axiom, in Algebra.Inter]
inter_com [lemma, in Algebra.Inter]
inter_assoc [lemma, in Algebra.Inter]
inter_comp [lemma, in Algebra.Inter]
inter_not_in_r [lemma, in Algebra.Inter]
inter_not_in_l [lemma, in Algebra.Inter]
inter_add_part_not_in [lemma, in Algebra.Fpart2]
inter_add_part [lemma, in Algebra.Fpart2]
inter_not_in [lemma, in Algebra.Fpart2]
Inter1 [section, in Algebra.Inter]
Inter1.E [variable, in Algebra.Inter]
Int_power.G [variable, in Algebra.Z_group]
Int_power [section, in Algebra.Z_group]
Int_power.G [variable, in Algebra.Group_power]
Int_power [section, in Algebra.Group_power]
inv [definition, in Algebra.Group_util]
Inv [constructor, in Algebra.Free_group]
Inv [constructor, in Algebra.Free_module]
Inv [constructor, in Algebra.Free_abelian_group]
Inverse [section, in Algebra.Group_cat]
inverse_l [definition, in Algebra.Group_cat]
inverse_r [definition, in Algebra.Group_cat]
Inverse_image1.f [variable, in Algebra.Parts3]
Inverse_image1.Inverse_image1_1.f [variable, in Algebra.Parts3]
Inverse_image1.Inverse_image1_1 [section, in Algebra.Parts3]
Inverse_image1.F [variable, in Algebra.Parts3]
Inverse_image1.E [variable, in Algebra.Parts3]
Inverse_image1 [section, in Algebra.Parts3]
Inverse.e [variable, in Algebra.Group_cat]
Inverse.f [variable, in Algebra.Group_cat]
Inverse.G [variable, in Algebra.Group_cat]
Inverse.inv [variable, in Algebra.Group_cat]
invfraction [definition, in Algebra.Fraction_field]
invfraction_fun [definition, in Algebra.Fraction_field]
invimage [definition, in Algebra.Parts3]
invimage_image_invimage [lemma, in Algebra.Parts3]
invimage_image [lemma, in Algebra.Parts3]
invimage_comp [lemma, in Algebra.Parts3]
invimage_included [lemma, in Algebra.Parts3]
invimage_in [lemma, in Algebra.Parts3]
invl [lemma, in Algebra.Group_util]
invr [lemma, in Algebra.Group_util]
in_image [lemma, in Algebra.Parts2]
in_compl [lemma, in Algebra.Parts2]
in_part_comp_r [lemma, in Algebra.Parts]
in_part_comp_l [lemma, in Algebra.Parts]
in_part [definition, in Algebra.Parts]
in_part_inter [lemma, in Algebra.Inter]
in_part_inter_r [lemma, in Algebra.Inter]
in_part_inter_l [lemma, in Algebra.Inter]
in_part_trans_eq [lemma, in Algebra.Fpart2]
in_diff [lemma, in Algebra.Fpart2]
in_eq_part [lemma, in Algebra.Fpart2]
in_invimage [lemma, in Algebra.Parts3]
in_single [lemma, in Algebra.Singleton]
in_part_union [lemma, in Algebra.Union]
in_part_union_or [axiom, in Algebra.Union]
in_part_union_r [lemma, in Algebra.Union]
in_part_union_l [lemma, in Algebra.Union]
is_ideal [definition, in Algebra.Ideal]
K
Ker [definition, in Algebra.Group_kernel]Ker [definition, in Algebra.Module_kernel]
kernel_normal [lemma, in Algebra.Group_kernel]
kernel_part [definition, in Algebra.Group_kernel]
Ker_prop_rev [lemma, in Algebra.Group_kernel]
Ker_prop [lemma, in Algebra.Group_kernel]
Ker_prop_rev [lemma, in Algebra.Module_kernel]
Ker_prop [lemma, in Algebra.Module_kernel]
L
Law [constructor, in Algebra.Free_monoid]Law [constructor, in Algebra.Free_group]
Law [constructor, in Algebra.Free_abelian_monoid]
Law [constructor, in Algebra.Free_module]
Law [constructor, in Algebra.Free_abelian_group]
law_of_composition [definition, in Algebra.Sgroup_cat]
Leibnitz_set_prop_rev [lemma, in Algebra.Sets]
Leibnitz_set_prop [lemma, in Algebra.Sets]
Leibnitz_set [definition, in Algebra.Sets]
Lemmas [section, in Algebra.Algebra_facts]
Lemmas [section, in Algebra.Group_facts]
Lemmas [section, in Algebra.Z_group_facts]
Lemmas [section, in Algebra.Integral_domain_facts]
Lemmas [section, in Algebra.Monoid_facts]
Lemmas [section, in Algebra.Ring_facts]
Lemmas [section, in Algebra.Group_power]
Lemmas [section, in Algebra.Module_facts]
Lemmas [section, in Algebra.Sgroup_facts]
Lemmas.A [variable, in Algebra.Algebra_facts]
Lemmas.E [variable, in Algebra.Monoid_facts]
Lemmas.E [variable, in Algebra.Sgroup_facts]
Lemmas.f [variable, in Algebra.Monoid_facts]
Lemmas.F [variable, in Algebra.Monoid_facts]
Lemmas.f [variable, in Algebra.Module_facts]
Lemmas.f [variable, in Algebra.Sgroup_facts]
Lemmas.F [variable, in Algebra.Sgroup_facts]
Lemmas.G [variable, in Algebra.Group_facts]
Lemmas.G [variable, in Algebra.Z_group_facts]
Lemmas.G [variable, in Algebra.Group_power]
Lemmas.Mod [variable, in Algebra.Module_facts]
Lemmas.Mod' [variable, in Algebra.Module_facts]
Lemmas.R [variable, in Algebra.Algebra_facts]
Lemmas.R [variable, in Algebra.Integral_domain_facts]
Lemmas.R [variable, in Algebra.Ring_facts]
Lemmas.R [variable, in Algebra.Module_facts]
Lemmas1 [section, in Algebra.Field_facts]
Lemmas1 [section, in Algebra.Cfield_facts]
Lemmas1.K [variable, in Algebra.Field_facts]
Lemmas1.K [variable, in Algebra.Cfield_facts]
Lemmas2 [section, in Algebra.Algebra_facts]
Lemmas2 [section, in Algebra.Group_facts]
Lemmas2.A [variable, in Algebra.Algebra_facts]
Lemmas2.f [variable, in Algebra.Group_facts]
Lemmas2.F [variable, in Algebra.Group_facts]
Lemmas2.G [variable, in Algebra.Group_facts]
Lemmas2.R [variable, in Algebra.Algebra_facts]
M
m [definition, in Algebra.Group_util]M [definition, in Algebra.Monoid_util]
M [definition, in Algebra.Ring_util]
MAP [definition, in Algebra.Sets]
Map [record, in Algebra.Sets]
Maps [section, in Algebra.Cartesian]
Maps.E [variable, in Algebra.Cartesian]
Maps.f [variable, in Algebra.Cartesian]
Maps.F [variable, in Algebra.Cartesian]
Maps.G [variable, in Algebra.Cartesian]
map_ext [lemma, in Algebra.Sets]
Map_eq [definition, in Algebra.Sets]
Map_compatible_prf [projection, in Algebra.Sets]
map_couple_proj_prop [lemma, in Algebra.Cartesian]
map_couple [definition, in Algebra.Cartesian]
map_proj2 [definition, in Algebra.Cartesian]
map_proj1 [definition, in Algebra.Cartesian]
map_not_injective [lemma, in Algebra.Fmap]
minus_add [lemma, in Algebra.Fpart]
minus_trans_not_in [lemma, in Algebra.Fpart]
minus_not_in [lemma, in Algebra.Fpart]
minus_part_com [lemma, in Algebra.Fpart]
minus_part_not_in [lemma, in Algebra.Fpart]
minus_part_comp [lemma, in Algebra.Fpart]
minus_part [definition, in Algebra.Fpart]
MODULE [definition, in Algebra.Module_cat]
module [record, in Algebra.Module_cat]
Module [section, in Algebra.Module_util]
module_id [definition, in Algebra.Module_cat]
module_hom_comp [definition, in Algebra.Module_cat]
module_hom_prf [projection, in Algebra.Module_cat]
module_monoid_hom [projection, in Algebra.Module_cat]
module_hom [record, in Algebra.Module_cat]
module_hom_prop [definition, in Algebra.Module_cat]
module_mult [definition, in Algebra.Module_cat]
module_on_def [projection, in Algebra.Module_cat]
module_carrier [projection, in Algebra.Module_cat]
module_op_lin_right_prf [projection, in Algebra.Module_cat]
module_op_lin_left_prf [projection, in Algebra.Module_cat]
module_op [projection, in Algebra.Module_cat]
module_on [record, in Algebra.Module_cat]
module_of_submodule [definition, in Algebra.Sub_module]
module_util_op2 [definition, in Algebra.Module_util]
module_util_endo_el2 [definition, in Algebra.Module_util]
Module_on_group.opunit [variable, in Algebra.Module_util]
Module_on_group.opassoc [variable, in Algebra.Module_util]
Module_on_group.oplin_r [variable, in Algebra.Module_util]
Module_on_group.oplin_l [variable, in Algebra.Module_util]
Module_on_group.op_comp [variable, in Algebra.Module_util]
Module_on_group.gen_module_op [variable, in Algebra.Module_util]
Module_on_group.module_util_G [variable, in Algebra.Module_util]
Module_on_group.R [variable, in Algebra.Module_util]
Module_on_group [section, in Algebra.Module_util]
module_util_G [definition, in Algebra.Module_util]
module_util_op [definition, in Algebra.Module_util]
module_util_endo_el [definition, in Algebra.Module_util]
MODULE_hom_prop [lemma, in Algebra.Module_facts]
MODULE_mult_op_l [lemma, in Algebra.Module_facts]
MODULE_mult_op_r [lemma, in Algebra.Module_facts]
MODULE_absorbant_r [lemma, in Algebra.Module_facts]
MODULE_absorbant_l [lemma, in Algebra.Module_facts]
MODULE_unit_l [lemma, in Algebra.Module_facts]
MODULE_dist_l [lemma, in Algebra.Module_facts]
MODULE_dist_r [lemma, in Algebra.Module_facts]
MODULE_assoc [lemma, in Algebra.Module_facts]
MODULE_comp [lemma, in Algebra.Module_facts]
Module_util [library]
Module_cat [library]
Module_facts [library]
Module_kernel [library]
Module.e [variable, in Algebra.Module_util]
Module.E [variable, in Algebra.Module_util]
Module.eunitgenlawr [variable, in Algebra.Module_util]
Module.fcom [variable, in Algebra.Module_util]
Module.fcomp [variable, in Algebra.Module_util]
Module.geninv [variable, in Algebra.Module_util]
Module.geninvr [variable, in Algebra.Module_util]
Module.genlaw [variable, in Algebra.Module_util]
Module.genlawassoc [variable, in Algebra.Module_util]
Module.gen_module_op [variable, in Algebra.Module_util]
Module.invcomp [variable, in Algebra.Module_util]
Module.opassoc [variable, in Algebra.Module_util]
Module.oplin_r [variable, in Algebra.Module_util]
Module.oplin_l [variable, in Algebra.Module_util]
Module.opunit [variable, in Algebra.Module_util]
Module.op_comp [variable, in Algebra.Module_util]
Module.R [variable, in Algebra.Module_util]
MONOID [definition, in Algebra.Monoid_cat]
monoid [record, in Algebra.Monoid_cat]
Monoid [section, in Algebra.Abelian_group_facts]
Monoid [section, in Algebra.Monoid_util]
monoid_id [definition, in Algebra.Monoid_cat]
monoid_hom_comp [definition, in Algebra.Monoid_cat]
monoid_hom_prf [projection, in Algebra.Monoid_cat]
monoid_sgroup_hom [projection, in Algebra.Monoid_cat]
monoid_hom [record, in Algebra.Monoid_cat]
monoid_hom_prop [definition, in Algebra.Monoid_cat]
monoid_on_def [projection, in Algebra.Monoid_cat]
monoid_sgroup [projection, in Algebra.Monoid_cat]
monoid_unit_l_prf [projection, in Algebra.Monoid_cat]
monoid_unit_r_prf [projection, in Algebra.Monoid_cat]
monoid_unit [projection, in Algebra.Monoid_cat]
monoid_on [record, in Algebra.Monoid_cat]
MONOID_hom_prop [lemma, in Algebra.Monoid_facts]
MONOID_unit_unique [lemma, in Algebra.Monoid_facts]
MONOID_unit_l [lemma, in Algebra.Monoid_facts]
MONOID_unit_r [lemma, in Algebra.Monoid_facts]
monoid_of_submonoid [definition, in Algebra.Sub_monoid]
Monoid_cat [library]
Monoid_facts [library]
Monoid_util [library]
Monoid_kernel [library]
Monoid.e [variable, in Algebra.Monoid_util]
Monoid.E [variable, in Algebra.Monoid_util]
Monoid.eunitgenlawl [variable, in Algebra.Monoid_util]
Monoid.eunitgenlawr [variable, in Algebra.Monoid_util]
Monoid.fcomp [variable, in Algebra.Monoid_util]
Monoid.genlaw [variable, in Algebra.Monoid_util]
Monoid.genlawassoc [variable, in Algebra.Monoid_util]
Monoid.M [variable, in Algebra.Abelian_group_facts]
multfraction_com [lemma, in Algebra.Fraction_field]
multfraction_dist_l [lemma, in Algebra.Fraction_field]
multfraction_fun [definition, in Algebra.Fraction_field]
mult_hom_module [definition, in Algebra.Hom_module]
N
nat_to_group_unit [lemma, in Algebra.Z_group_facts]nat_to_group_mult [lemma, in Algebra.Z_group_facts]
nat_to_group_comp [lemma, in Algebra.Z_group_facts]
nat_to_group_mult [lemma, in Algebra.ZUP]
nat_to_group_inverse [lemma, in Algebra.Z_group]
nat_to_group_com4 [lemma, in Algebra.Z_group]
nat_to_group_com3 [lemma, in Algebra.Z_group]
nat_to_group_minus [lemma, in Algebra.Z_group]
nat_to_group_com2 [lemma, in Algebra.Z_group]
nat_to_group_add [lemma, in Algebra.Z_group]
nat_to_group_com [lemma, in Algebra.Z_group]
nat_to_group [definition, in Algebra.Z_group]
normal [definition, in Algebra.Group_quotient]
normal_com_in [lemma, in Algebra.Group_quotient]
not_in_compl [lemma, in Algebra.Parts2]
not_in_comp_r [lemma, in Algebra.Parts2]
not_in_comp_l [lemma, in Algebra.Parts2]
not_inpart_comp_r [lemma, in Algebra.Parts]
not_in_part_trans_eq [lemma, in Algebra.Fpart]
not_in_part_trans [lemma, in Algebra.Fpart]
not_in_empty [lemma, in Algebra.Fpart]
not_included_exist [lemma, in Algebra.Fmap]
not_in_part_comp_r [axiom, in Algebra.Fmap]
not_surjective_prop [lemma, in Algebra.Fmap]
not_injective_prop [lemma, in Algebra.Fmap]
num [projection, in Algebra.Fraction_field]
O
Ob [projection, in Algebra.Categories]Objects [section, in Algebra.Integral_domain_cat]
Objects [section, in Algebra.Ring_cat]
Op [constructor, in Algebra.Free_module]
operation [definition, in Algebra.Operation_of_monoid]
operation_unit [lemma, in Algebra.Operation_of_monoid]
operation_assoc [lemma, in Algebra.Operation_of_monoid]
Operation_of_monoid [library]
opfraction_fun [definition, in Algebra.Fraction_field]
opp_hom_module [definition, in Algebra.Hom_module]
op_lin_right [definition, in Algebra.Module_cat]
op_lin_left [definition, in Algebra.Module_cat]
P
part [definition, in Algebra.Parts]partial_equivalence [definition, in Algebra.Sets]
Parts [library]
Parts2 [library]
Parts3 [library]
part_set_is_strictly_greater_than_set [lemma, in Algebra.Parts]
part_set_is_strictly_greater_than_set1 [lemma, in Algebra.Parts]
Part_set_greater.invX [variable, in Algebra.Parts]
Part_set_greater.X [variable, in Algebra.Parts]
Part_set_greater.X_def [variable, in Algebra.Parts]
Part_set_greater.fsurj [variable, in Algebra.Parts]
Part_set_greater.f [variable, in Algebra.Parts]
Part_set_greater.E [variable, in Algebra.Parts]
Part_set_greater [section, in Algebra.Parts]
part_set [definition, in Algebra.Parts]
Part_set.eq_part_equiv [variable, in Algebra.Parts]
Part_set.E [variable, in Algebra.Parts]
Part_set [section, in Algebra.Parts]
Part_type.P [variable, in Algebra.Parts]
Part_type.E [variable, in Algebra.Parts]
Part_type [section, in Algebra.Parts]
pos_abs_comp [lemma, in Algebra.Z_group_facts]
pos_nat_group [lemma, in Algebra.Z_group]
pos_to_group [definition, in Algebra.Z_group]
pos_abs_ok [lemma, in Algebra.Z_group]
pos_abs [definition, in Algebra.Z_group]
Predicate [record, in Algebra.Parts]
Pred_compatible_prf [projection, in Algebra.Parts]
Pred_fun [projection, in Algebra.Parts]
pred_compatible [definition, in Algebra.Parts]
Prf_equiv [projection, in Algebra.Sets]
Projections [section, in Algebra.Cartesian]
Projections.E [variable, in Algebra.Cartesian]
Projections.F [variable, in Algebra.Cartesian]
proj1 [definition, in Algebra.Cartesian]
proj1_map [definition, in Algebra.Cartesian]
proj1_comp [lemma, in Algebra.Cartesian]
proj2 [definition, in Algebra.Cartesian]
proj2_map [definition, in Algebra.Cartesian]
proj2_comp [lemma, in Algebra.Cartesian]
Q
Q [definition, in Algebra.Qfield]Qfield [library]
quotient [definition, in Algebra.Sets]
R
real [projection, in Algebra.Complex_field]real_comp [lemma, in Algebra.Complex_field]
Refl [lemma, in Algebra.Sets]
reflexive [definition, in Algebra.Sets]
Relation [record, in Algebra.Sets]
relation [definition, in Algebra.Sets]
Rel_comp [lemma, in Algebra.Sets]
Rel_compatible_prf [projection, in Algebra.Sets]
Rel_fun [projection, in Algebra.Sets]
rel_compatible [definition, in Algebra.Sets]
restrict [definition, in Algebra.Parts3]
Restrictions1 [section, in Algebra.Parts3]
Restrictions1.E [variable, in Algebra.Parts3]
Restrictions1.f [variable, in Algebra.Parts3]
Restrictions1.F [variable, in Algebra.Parts3]
restrict_prop_in_part [lemma, in Algebra.Parts3]
restrict_prop [lemma, in Algebra.Parts3]
RING [definition, in Algebra.Ring_cat]
ring [record, in Algebra.Ring_cat]
Ring [section, in Algebra.Ring_util]
ring_algebra_ring [definition, in Algebra.Algebra_facts]
Ring_algebra_as_ring.A [variable, in Algebra.Algebra_facts]
Ring_algebra_as_ring.R [variable, in Algebra.Algebra_facts]
Ring_algebra_as_ring [section, in Algebra.Algebra_facts]
RING_ALGEBRA_unit_r [lemma, in Algebra.Algebra_facts]
RING_ALGEBRA_unit_l [lemma, in Algebra.Algebra_facts]
RING_ALGEBRA_assoc [lemma, in Algebra.Algebra_facts]
ring_algebra_on_def [projection, in Algebra.Algebra]
ring_algebra_algebra [projection, in Algebra.Algebra]
ring_algebra [record, in Algebra.Algebra]
ring_algebra_unit_r [projection, in Algebra.Algebra]
ring_algebra_unit_l [projection, in Algebra.Algebra]
ring_algebra_unit [projection, in Algebra.Algebra]
ring_algebra_assoc [projection, in Algebra.Algebra]
ring_algebra_on [record, in Algebra.Algebra]
ring_id [definition, in Algebra.Ring_cat]
ring_hom_comp [definition, in Algebra.Ring_cat]
ring_mult_hom_prf [projection, in Algebra.Ring_cat]
ring_mult_hom_unit [projection, in Algebra.Ring_cat]
ring_plus_hom [projection, in Algebra.Ring_cat]
ring_hom [record, in Algebra.Ring_cat]
ring_mult_hom_prop [definition, in Algebra.Ring_cat]
ring_mult_hom_unit_prop [definition, in Algebra.Ring_cat]
ring_unit [definition, in Algebra.Ring_cat]
ring_mult [definition, in Algebra.Ring_cat]
ring_on_def [projection, in Algebra.Ring_cat]
ring_group [projection, in Algebra.Ring_cat]
ring_dist_l_prf [projection, in Algebra.Ring_cat]
ring_dist_r_prf [projection, in Algebra.Ring_cat]
ring_monoid [projection, in Algebra.Ring_cat]
ring_mult_monoid [projection, in Algebra.Ring_cat]
ring_mult_sgroup [projection, in Algebra.Ring_cat]
ring_on [record, in Algebra.Ring_cat]
ring_module [definition, in Algebra.Ideal]
Ring_as_module.R [variable, in Algebra.Ideal]
Ring_as_module [section, in Algebra.Ideal]
RING_hom_ext [lemma, in Algebra.Ring_facts]
RING_one_prop [lemma, in Algebra.Ring_facts]
RING_hom_prop [lemma, in Algebra.Ring_facts]
RING_op_mult_r [lemma, in Algebra.Ring_facts]
RING_op_mult_l [lemma, in Algebra.Ring_facts]
RING_absorbant_l [lemma, in Algebra.Ring_facts]
RING_absorbant_r [lemma, in Algebra.Ring_facts]
RING_dist_l [lemma, in Algebra.Ring_facts]
RING_dist_r [lemma, in Algebra.Ring_facts]
RING_unit_l [lemma, in Algebra.Ring_facts]
RING_unit_r [lemma, in Algebra.Ring_facts]
RING_comp [lemma, in Algebra.Ring_facts]
RING_assoc [lemma, in Algebra.Ring_facts]
Ring_cat [library]
Ring_facts [library]
Ring_util [library]
Ring.E [variable, in Algebra.Ring_util]
Ring.oppcomp [variable, in Algebra.Ring_util]
Ring.ringdistl [variable, in Algebra.Ring_util]
Ring.ringdistr [variable, in Algebra.Ring_util]
Ring.ringmult [variable, in Algebra.Ring_util]
Ring.ringmultassoc [variable, in Algebra.Ring_util]
Ring.ringmultcomp [variable, in Algebra.Ring_util]
Ring.ringopp [variable, in Algebra.Ring_util]
Ring.ringoppr [variable, in Algebra.Ring_util]
Ring.ringplus [variable, in Algebra.Ring_util]
Ring.ringplusassoc [variable, in Algebra.Ring_util]
Ring.ringpluscom [variable, in Algebra.Ring_util]
Ring.ringpluscomp [variable, in Algebra.Ring_util]
Ring.un [variable, in Algebra.Ring_util]
Ring.ununitlringmult [variable, in Algebra.Ring_util]
Ring.ununitringmultr [variable, in Algebra.Ring_util]
Ring.zero [variable, in Algebra.Ring_util]
Ring.zerounitringplusr [variable, in Algebra.Ring_util]
S
SET [definition, in Algebra.Set_cat]Setoid [record, in Algebra.Sets]
Sets [library]
Sets1 [section, in Algebra.Sets]
Sets1.eqT_equiv [variable, in Algebra.Sets]
Sets1.Maps1 [section, in Algebra.Sets]
Sets1.Maps1.Maps1_3.f [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_3.g [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_3.G [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_3.F [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_3.E [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_3 [section, in Algebra.Sets]
Sets1.Maps1.Maps1_2.B [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_2.A [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_2 [section, in Algebra.Sets]
Sets1.Maps1.Maps1_1.Map_eq_equiv [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_1.B [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_1.A [variable, in Algebra.Sets]
Sets1.Maps1.Maps1_1 [section, in Algebra.Sets]
Sets1.Quotient1 [section, in Algebra.Sets]
Sets1.Quotient1.E [variable, in Algebra.Sets]
Sets1.Quotient1.R [variable, in Algebra.Sets]
Sets1.Quotient1.R_equiv [variable, in Algebra.Sets]
Sets1.Relations [section, in Algebra.Sets]
Sets1.Relations.E [variable, in Algebra.Sets]
set_full_set [lemma, in Algebra.Parts]
set_to_full [definition, in Algebra.Parts]
set_of_subtype_image [definition, in Algebra.Parts]
Set_cat [library]
sg [definition, in Algebra.Group_util]
sg [definition, in Algebra.Monoid_util]
SGROUP [definition, in Algebra.Sgroup_cat]
sgroup [record, in Algebra.Sgroup_cat]
Sgroup [section, in Algebra.Abelian_group_facts]
sgroup_of_subsgroup [definition, in Algebra.Sub_sgroup]
sgroup_id [definition, in Algebra.Sgroup_cat]
sgroup_hom_comp [definition, in Algebra.Sgroup_cat]
sgroup_hom_prf [projection, in Algebra.Sgroup_cat]
sgroup_map [projection, in Algebra.Sgroup_cat]
sgroup_hom [record, in Algebra.Sgroup_cat]
sgroup_hom_prop [definition, in Algebra.Sgroup_cat]
sgroup_law [definition, in Algebra.Sgroup_cat]
sgroup_on_def [projection, in Algebra.Sgroup_cat]
sgroup_set [projection, in Algebra.Sgroup_cat]
sgroup_assoc_prf [projection, in Algebra.Sgroup_cat]
sgroup_law_map [projection, in Algebra.Sgroup_cat]
sgroup_on [record, in Algebra.Sgroup_cat]
sgroup_powers_rev [lemma, in Algebra.Z_group]
sgroup_powers_prop [lemma, in Algebra.Z_group]
sgroup_powers [definition, in Algebra.Z_group]
SGROUP_hom_prop [lemma, in Algebra.Sgroup_facts]
SGROUP_comp [lemma, in Algebra.Sgroup_facts]
SGROUP_assoc [lemma, in Algebra.Sgroup_facts]
Sgroup_facts [library]
Sgroup_cat [library]
Sgroup.S [variable, in Algebra.Abelian_group_facts]
single [definition, in Algebra.Singleton]
Singleton [library]
single_add [lemma, in Algebra.Fpart]
single_simpl [lemma, in Algebra.Singleton]
single_prop_rev [lemma, in Algebra.Singleton]
single_prop [lemma, in Algebra.Singleton]
single_law [lemma, in Algebra.Singleton]
Single1 [section, in Algebra.Singleton]
Single1.E [variable, in Algebra.Singleton]
subcat [definition, in Algebra.Subcat]
Subcat [library]
Subcategory_def.CompC'_ok [variable, in Algebra.Subcat]
Subcategory_def.idC'ok [variable, in Algebra.Subcat]
Subcategory_def.idC' [variable, in Algebra.Subcat]
Subcategory_def.CompC' [variable, in Algebra.Subcat]
Subcategory_def.homC' [variable, in Algebra.Subcat]
Subcategory_def.i [variable, in Algebra.Subcat]
Subcategory_def.C' [variable, in Algebra.Subcat]
Subcategory_def.C [variable, in Algebra.Subcat]
Subcategory_def [section, in Algebra.Subcat]
subcat_Hom_comp [definition, in Algebra.Subcat]
subcat_Hom [definition, in Algebra.Subcat]
subgroup [record, in Algebra.Sub_group]
subgroup_in_prop [lemma, in Algebra.Sub_group]
subgroup_prop [projection, in Algebra.Sub_group]
subgroup_submonoid [projection, in Algebra.Sub_group]
subgroup_group [definition, in Algebra.Sub_group]
subgroup_inv [definition, in Algebra.Sub_group]
submodule [record, in Algebra.Sub_module]
submodule_in_prop [lemma, in Algebra.Sub_module]
submodule_prop [projection, in Algebra.Sub_module]
submodule_subgroup [projection, in Algebra.Sub_module]
submodule_module [definition, in Algebra.Sub_module]
submodule_op [definition, in Algebra.Sub_module]
submonoid [record, in Algebra.Sub_monoid]
submonoid_in_prop [lemma, in Algebra.Sub_monoid]
submonoid_prop [projection, in Algebra.Sub_monoid]
submonoid_subsgroup [projection, in Algebra.Sub_monoid]
submonoid_monoid [definition, in Algebra.Sub_monoid]
subsgroup [record, in Algebra.Sub_sgroup]
subsgroup_in_prop [lemma, in Algebra.Sub_sgroup]
subsgroup_prop [projection, in Algebra.Sub_sgroup]
subsgroup_part [projection, in Algebra.Sub_sgroup]
subsgroup_sgroup [definition, in Algebra.Sub_sgroup]
subsgroup_law [definition, in Algebra.Sub_sgroup]
subtype [record, in Algebra.Parts]
Subtype [section, in Algebra.Parts]
subtype_prf [projection, in Algebra.Parts]
subtype_elt [projection, in Algebra.Parts]
subtype_image_inj [projection, in Algebra.Parts]
subtype_image_carrier [projection, in Algebra.Parts]
subtype_image [record, in Algebra.Parts]
subtype_image_set [definition, in Algebra.Parts]
subtype_image_equiv [lemma, in Algebra.Parts]
subtype_image_equal [definition, in Algebra.Parts]
Subtype.E [variable, in Algebra.Parts]
Subtype.F [variable, in Algebra.Parts]
Subtype.i [variable, in Algebra.Parts]
Sub_module [library]
Sub_monoid [library]
Sub_sgroup [library]
Sub_group [library]
surjective [definition, in Algebra.Sets]
surjective_comp [lemma, in Algebra.Sets]
surjective_image_full [axiom, in Algebra.Fmap]
surj_part_image_surjective [lemma, in Algebra.Parts2]
surj_part_image [definition, in Algebra.Parts2]
surj_set_image_surjective [lemma, in Algebra.Parts2]
surj_set_image [definition, in Algebra.Parts2]
surj_set_quo_surjective [lemma, in Algebra.Sets]
surj_set_quo [definition, in Algebra.Sets]
surj_group_quo_ker_surjective [lemma, in Algebra.Group_hom_factor]
surj_group_quo_ker [definition, in Algebra.Group_hom_factor]
Sym [lemma, in Algebra.Sets]
symmetric [definition, in Algebra.Sets]
T
tiroirs [lemma, in Algebra.Tiroirs]Tiroirs [library]
tiroirs_def.f [variable, in Algebra.Tiroirs]
tiroirs_def.F [variable, in Algebra.Tiroirs]
tiroirs_def.E [variable, in Algebra.Tiroirs]
tiroirs_def [section, in Algebra.Tiroirs]
Trans [lemma, in Algebra.Sets]
transitive [definition, in Algebra.Sets]
U
uncurry [definition, in Algebra.Cartesian]union [definition, in Algebra.Union]
Union [library]
union_part_upper_bound [lemma, in Algebra.Parts]
union_part_included [lemma, in Algebra.Parts]
union_part_prop_rev [lemma, in Algebra.Parts]
union_part_prop [lemma, in Algebra.Parts]
union_part [definition, in Algebra.Parts]
Union_of_part.P [variable, in Algebra.Parts]
Union_of_part.E [variable, in Algebra.Parts]
Union_of_part [section, in Algebra.Parts]
union_diff [lemma, in Algebra.Fpart2]
union_not_in [lemma, in Algebra.Fpart2]
union_unit_l [lemma, in Algebra.Fpart]
union_single_in [axiom, in Algebra.Fmap]
union_empty_r [axiom, in Algebra.Union]
union_empty_l [axiom, in Algebra.Union]
union_com [lemma, in Algebra.Union]
union_assoc [lemma, in Algebra.Union]
union_comp [lemma, in Algebra.Union]
union_not_in_l [lemma, in Algebra.Union]
Union1 [section, in Algebra.Union]
Union1.E [variable, in Algebra.Union]
Unit [constructor, in Algebra.Free_monoid]
Unit [constructor, in Algebra.Free_group]
Unit [constructor, in Algebra.Free_abelian_monoid]
Unit [section, in Algebra.Monoid_cat]
Unit [constructor, in Algebra.Free_module]
Unit [constructor, in Algebra.Free_abelian_group]
unit_l [definition, in Algebra.Monoid_cat]
unit_r [definition, in Algebra.Monoid_cat]
Unit.e [variable, in Algebra.Monoid_cat]
Unit.E [variable, in Algebra.Monoid_cat]
Unit.f [variable, in Algebra.Monoid_cat]
V
Var [constructor, in Algebra.Free_monoid]Var [constructor, in Algebra.Free_group]
Var [constructor, in Algebra.Free_abelian_monoid]
Var [constructor, in Algebra.Free_module]
Var [constructor, in Algebra.Free_abelian_group]
Z
zero_hom_module [definition, in Algebra.Hom_module]Zlemma1 [lemma, in Algebra.Z_group]
Zlt_reg_l [lemma, in Algebra.Z_group]
Zl1 [lemma, in Algebra.Z_group]
Zl2 [lemma, in Algebra.Z_group]
Zl3 [lemma, in Algebra.Z_group]
Zl4 [lemma, in Algebra.Z_group]
Zl5 [lemma, in Algebra.Z_group]
Zopp1 [lemma, in Algebra.Z_group_facts]
Zopp2 [lemma, in Algebra.Z_group_facts]
Zr [definition, in Algebra.Zring]
Zring [library]
Zr_aux [definition, in Algebra.Zring]
ZUP [library]
Zup1 [section, in Algebra.ZUP]
Zup1 [section, in Algebra.Z_group]
Zup1.G [variable, in Algebra.Z_group]
Zup1.R [variable, in Algebra.ZUP]
Zup1.r [variable, in Algebra.Z_group]
Zup2 [section, in Algebra.Z_group]
Zup2.G [variable, in Algebra.Z_group]
Zup2.pos_def.r [variable, in Algebra.Z_group]
Zup2.pos_def [section, in Algebra.Z_group]
Zup2.r [variable, in Algebra.Z_group]
ZZ [definition, in Algebra.Zring]
Zzero_dec [definition, in Algebra.Zring]
Z_group_nat_fun_mult_pos [lemma, in Algebra.Z_group_facts]
Z_to_group_nat_unit [lemma, in Algebra.Z_group_facts]
Z_to_group_nat_inv [lemma, in Algebra.Z_group_facts]
Z_to_group_nat_neg [lemma, in Algebra.Z_group_facts]
Z_to_group_nat_fun_comp [lemma, in Algebra.Z_group_facts]
Z_to_group_nat_eq_pos [lemma, in Algebra.Z_group_facts]
Z_one_diff_zero [lemma, in Algebra.Qfield]
Z_to_ring [definition, in Algebra.ZUP]
Z_to_group [definition, in Algebra.Z_group]
Z_to_group_fun_eq [lemma, in Algebra.Z_group]
Z_to_group_fun [definition, in Algebra.Z_group]
Z_to_group_nat [definition, in Algebra.Z_group]
Z_to_group_nat_fun [definition, in Algebra.Z_group]
Z_group [library]
Z_group_facts [library]
Variable Index
A
Abelian_group.fcom [in Algebra.Group_util]Abelian_group.geninvr [in Algebra.Group_util]
Abelian_group.invcomp [in Algebra.Group_util]
Abelian_group.eunitgenlawr [in Algebra.Group_util]
Abelian_group.genlawassoc [in Algebra.Group_util]
Abelian_group.fcomp [in Algebra.Group_util]
Abelian_group.geninv [in Algebra.Group_util]
Abelian_group.e [in Algebra.Group_util]
Abelian_group.genlaw [in Algebra.Group_util]
Abelian_group.E [in Algebra.Group_util]
Abelian_monoid.fcom [in Algebra.Monoid_util]
Abelian_monoid.eunitgenlawl [in Algebra.Monoid_util]
Abelian_monoid.eunitgenlawr [in Algebra.Monoid_util]
Abelian_monoid.genlawassoc [in Algebra.Monoid_util]
Abelian_monoid.fcomp [in Algebra.Monoid_util]
Abelian_monoid.e [in Algebra.Monoid_util]
Abelian_monoid.genlaw [in Algebra.Monoid_util]
Abelian_monoid.E [in Algebra.Monoid_util]
algebra_def.R [in Algebra.Algebra]
B
Build_sub_group.Hinv [in Algebra.Group_util]Build_sub_group.Hunit [in Algebra.Group_util]
Build_sub_group.Hlaw [in Algebra.Group_util]
Build_sub_group.H [in Algebra.Group_util]
Build_sub_group.G [in Algebra.Group_util]
Build_sub_monoid.Hunit [in Algebra.Monoid_util]
Build_sub_monoid.Hlaw [in Algebra.Monoid_util]
Build_sub_monoid.H [in Algebra.Monoid_util]
Build_sub_monoid.G [in Algebra.Monoid_util]
C
Cantor_Bernstein.map_extend [in Algebra.Cantor_Bernstein]Cantor_Bernstein.partial_section [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.img [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.PXeq [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.hXX [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.XhX [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.X [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.PX [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.h_incr [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.h [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.ginj [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.finj [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.g [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.f [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.F [in Algebra.Cantor_Bernstein]
Cantor_Bernstein.E [in Algebra.Cantor_Bernstein]
Category_def.Full_subcat_def.i [in Algebra.Categories]
Category_def.Full_subcat_def.C' [in Algebra.Categories]
Category_def.Full_subcat_def.C [in Algebra.Categories]
Category_def.Category_comp.C [in Algebra.Categories]
Category_def.Category_def1.Hom_id [in Algebra.Categories]
Category_def.Category_def1.Hom_comp [in Algebra.Categories]
Category_def.Category_def1.Hom [in Algebra.Categories]
Category_def.Category_def1.Ob [in Algebra.Categories]
Commutative_rings.R1 [in Algebra.Ring_facts]
Complement1.E [in Algebra.Parts2]
D
Def.diff10 [in Algebra.Fraction_field]Def.E [in Algebra.Endo_set]
Def.E [in Algebra.Cartesian]
Def.f [in Algebra.Group_kernel]
Def.f [in Algebra.Group_hom_factor]
Def.F [in Algebra.Cartesian]
Def.f [in Algebra.Module_kernel]
Def.ff_field_on [in Algebra.Fraction_field]
Def.ff_inr_r [in Algebra.Fraction_field]
Def.G [in Algebra.Sub_group]
Def.G [in Algebra.Group_kernel]
Def.G [in Algebra.Group_quotient]
Def.G [in Algebra.Group_of_group_hom]
Def.G [in Algebra.Group_hom_factor]
Def.G [in Algebra.Sub_sgroup]
Def.G [in Algebra.Sub_monoid]
Def.G' [in Algebra.Group_kernel]
Def.G' [in Algebra.Group_of_group_hom]
Def.G' [in Algebra.Group_hom_factor]
Def.H [in Algebra.Group_quotient]
Def.Hnormal [in Algebra.Group_quotient]
Def.Hom.E [in Algebra.Module_cat]
Def.Hom.F [in Algebra.Module_cat]
Def.M [in Algebra.Sub_module]
Def.M [in Algebra.Operation_of_monoid]
Def.Mod [in Algebra.Module_kernel]
Def.Module_def.op [in Algebra.Module_cat]
Def.Module_def.Mod [in Algebra.Module_cat]
Def.Mod2 [in Algebra.Module_kernel]
Def.op [in Algebra.Operation_of_monoid]
Def.R [in Algebra.Module_cat]
Def.R [in Algebra.Complex_field]
Def.R [in Algebra.Sub_module]
Def.R [in Algebra.Fraction_field]
Def.R [in Algebra.Module_kernel]
Def.S [in Algebra.Operation_of_monoid]
Def.Sub_module.endofun [in Algebra.Sub_module]
Def.Sub_module.Na [in Algebra.Sub_module]
Def.Sub_module.Nop [in Algebra.Sub_module]
Def.Sub_module.N [in Algebra.Sub_module]
Def.Sub_group.Hinv [in Algebra.Sub_group]
Def.Sub_group.H [in Algebra.Sub_group]
Def.Sub_sgroup.Hprop [in Algebra.Sub_sgroup]
Def.Sub_sgroup.H [in Algebra.Sub_sgroup]
Def.Sub_monoid.Hunit [in Algebra.Sub_monoid]
Def.Sub_monoid.H [in Algebra.Sub_monoid]
Def.sum_of_square [in Algebra.Complex_field]
Def.zero_dec [in Algebra.Fraction_field]
Diff.E [in Algebra.Diff]
F
Foncteurs.Def_1.C2 [in Algebra.Categories2]Foncteurs.Def_1.C1 [in Algebra.Categories2]
fparts_in_def.E [in Algebra.Fpart]
fparts2_def.E [in Algebra.Fpart2]
Free_monoid_def.Universal_prop.f [in Algebra.Free_monoid]
Free_monoid_def.Universal_prop.M [in Algebra.Free_monoid]
Free_monoid_def.V [in Algebra.Free_monoid]
Free_group_def.Universal_prop.f [in Algebra.Free_group]
Free_group_def.Universal_prop.G [in Algebra.Free_group]
Free_group_def.V [in Algebra.Free_group]
Free_abelian_monoid_def.Universal_prop.f [in Algebra.Free_abelian_monoid]
Free_abelian_monoid_def.Universal_prop.M [in Algebra.Free_abelian_monoid]
Free_abelian_monoid_def.V [in Algebra.Free_abelian_monoid]
Free_Module_def.Universal_prop.f [in Algebra.Free_module]
Free_Module_def.Universal_prop.Mod [in Algebra.Free_module]
Free_Module_def.V [in Algebra.Free_module]
Free_Module_def.R [in Algebra.Free_module]
Free_abelian_group_def.Universal_prop.f [in Algebra.Free_abelian_group]
Free_abelian_group_def.Universal_prop.G [in Algebra.Free_abelian_group]
Free_abelian_group_def.V [in Algebra.Free_abelian_group]
G
Generated_monoid_def.A [in Algebra.Generated_monoid]Generated_monoid_def.M [in Algebra.Generated_monoid]
Generated_group_def.A [in Algebra.Generated_group]
Generated_group_def.G [in Algebra.Generated_group]
Generated_ideal.A [in Algebra.Ideal]
Generated_ideal.R [in Algebra.Ideal]
Generated_module_def.A [in Algebra.Generated_module]
Generated_module_def.Mod [in Algebra.Generated_module]
Generated_module_def.R [in Algebra.Generated_module]
Group.e [in Algebra.Group_util]
Group.E [in Algebra.Group_util]
Group.eunitgenlawr [in Algebra.Group_util]
Group.fcomp [in Algebra.Group_util]
Group.G [in Algebra.Abelian_group_facts]
Group.geninv [in Algebra.Group_util]
Group.geninvr [in Algebra.Group_util]
Group.genlaw [in Algebra.Group_util]
Group.genlawassoc [in Algebra.Group_util]
Group.invcomp [in Algebra.Group_util]
H
Hom_module_def.Mod2 [in Algebra.Hom_module]Hom_module_def.Mod1 [in Algebra.Hom_module]
Hom_module_def.R [in Algebra.Hom_module]
Hom_lemmas.f [in Algebra.Ring_facts]
Hom_lemmas.R' [in Algebra.Ring_facts]
Hom_lemmas.R [in Algebra.Ring_facts]
Hom.E [in Algebra.Ring_cat]
Hom.E [in Algebra.Monoid_cat]
Hom.E [in Algebra.Sgroup_cat]
Hom.F [in Algebra.Ring_cat]
Hom.F [in Algebra.Monoid_cat]
Hom.F [in Algebra.Sgroup_cat]
Hom.ff [in Algebra.Group_util]
Hom.ff [in Algebra.Module_util]
Hom.ff [in Algebra.Monoid_util]
Hom.ff [in Algebra.Ring_util]
Hom.ffcomp [in Algebra.Group_util]
Hom.ffcomp [in Algebra.Module_util]
Hom.ffcomp [in Algebra.Monoid_util]
Hom.ffcomp [in Algebra.Ring_util]
Hom.fflaw [in Algebra.Group_util]
Hom.fflaw [in Algebra.Module_util]
Hom.fflaw [in Algebra.Monoid_util]
Hom.ffmult [in Algebra.Ring_util]
Hom.ffone [in Algebra.Ring_util]
Hom.ffop [in Algebra.Module_util]
Hom.ffplus [in Algebra.Ring_util]
Hom.ffunit [in Algebra.Group_util]
Hom.ffunit [in Algebra.Module_util]
Hom.ffunit [in Algebra.Monoid_util]
Hom.ffzero [in Algebra.Ring_util]
Hom.G [in Algebra.Group_util]
Hom.G [in Algebra.Monoid_util]
Hom.G' [in Algebra.Group_util]
Hom.G' [in Algebra.Monoid_util]
Hom.Mod [in Algebra.Module_util]
Hom.Mod' [in Algebra.Module_util]
Hom.R [in Algebra.Module_util]
Hom.Ring1 [in Algebra.Ring_util]
Hom.Ring2 [in Algebra.Ring_util]
I
ideals.R [in Algebra.Ideal]Images1.E [in Algebra.Parts2]
Images1.f [in Algebra.Parts2]
Images1.F [in Algebra.Parts2]
Images1.surj_part_image_fun [in Algebra.Parts2]
Images1.surj_set_image_fun [in Algebra.Parts2]
Image_hom.f [in Algebra.Monoid_kernel]
Image_hom.M' [in Algebra.Monoid_kernel]
Image_hom.M [in Algebra.Monoid_kernel]
Inclusion.E [in Algebra.Parts]
Injection.G [in Algebra.Sub_group]
Injection.G [in Algebra.Sub_sgroup]
Injection.G [in Algebra.Sub_monoid]
Injection.H [in Algebra.Sub_group]
Injection.H [in Algebra.Sub_sgroup]
Injection.H [in Algebra.Sub_monoid]
Injection.M [in Algebra.Sub_module]
Injection.N [in Algebra.Sub_module]
Injection.R [in Algebra.Sub_module]
Inter1.E [in Algebra.Inter]
Int_power.G [in Algebra.Z_group]
Int_power.G [in Algebra.Group_power]
Inverse_image1.f [in Algebra.Parts3]
Inverse_image1.Inverse_image1_1.f [in Algebra.Parts3]
Inverse_image1.F [in Algebra.Parts3]
Inverse_image1.E [in Algebra.Parts3]
Inverse.e [in Algebra.Group_cat]
Inverse.f [in Algebra.Group_cat]
Inverse.G [in Algebra.Group_cat]
Inverse.inv [in Algebra.Group_cat]
L
Lemmas.A [in Algebra.Algebra_facts]Lemmas.E [in Algebra.Monoid_facts]
Lemmas.E [in Algebra.Sgroup_facts]
Lemmas.f [in Algebra.Monoid_facts]
Lemmas.F [in Algebra.Monoid_facts]
Lemmas.f [in Algebra.Module_facts]
Lemmas.f [in Algebra.Sgroup_facts]
Lemmas.F [in Algebra.Sgroup_facts]
Lemmas.G [in Algebra.Group_facts]
Lemmas.G [in Algebra.Z_group_facts]
Lemmas.G [in Algebra.Group_power]
Lemmas.Mod [in Algebra.Module_facts]
Lemmas.Mod' [in Algebra.Module_facts]
Lemmas.R [in Algebra.Algebra_facts]
Lemmas.R [in Algebra.Integral_domain_facts]
Lemmas.R [in Algebra.Ring_facts]
Lemmas.R [in Algebra.Module_facts]
Lemmas1.K [in Algebra.Field_facts]
Lemmas1.K [in Algebra.Cfield_facts]
Lemmas2.A [in Algebra.Algebra_facts]
Lemmas2.f [in Algebra.Group_facts]
Lemmas2.F [in Algebra.Group_facts]
Lemmas2.G [in Algebra.Group_facts]
Lemmas2.R [in Algebra.Algebra_facts]
M
Maps.E [in Algebra.Cartesian]Maps.f [in Algebra.Cartesian]
Maps.F [in Algebra.Cartesian]
Maps.G [in Algebra.Cartesian]
Module_on_group.opunit [in Algebra.Module_util]
Module_on_group.opassoc [in Algebra.Module_util]
Module_on_group.oplin_r [in Algebra.Module_util]
Module_on_group.oplin_l [in Algebra.Module_util]
Module_on_group.op_comp [in Algebra.Module_util]
Module_on_group.gen_module_op [in Algebra.Module_util]
Module_on_group.module_util_G [in Algebra.Module_util]
Module_on_group.R [in Algebra.Module_util]
Module.e [in Algebra.Module_util]
Module.E [in Algebra.Module_util]
Module.eunitgenlawr [in Algebra.Module_util]
Module.fcom [in Algebra.Module_util]
Module.fcomp [in Algebra.Module_util]
Module.geninv [in Algebra.Module_util]
Module.geninvr [in Algebra.Module_util]
Module.genlaw [in Algebra.Module_util]
Module.genlawassoc [in Algebra.Module_util]
Module.gen_module_op [in Algebra.Module_util]
Module.invcomp [in Algebra.Module_util]
Module.opassoc [in Algebra.Module_util]
Module.oplin_r [in Algebra.Module_util]
Module.oplin_l [in Algebra.Module_util]
Module.opunit [in Algebra.Module_util]
Module.op_comp [in Algebra.Module_util]
Module.R [in Algebra.Module_util]
Monoid.e [in Algebra.Monoid_util]
Monoid.E [in Algebra.Monoid_util]
Monoid.eunitgenlawl [in Algebra.Monoid_util]
Monoid.eunitgenlawr [in Algebra.Monoid_util]
Monoid.fcomp [in Algebra.Monoid_util]
Monoid.genlaw [in Algebra.Monoid_util]
Monoid.genlawassoc [in Algebra.Monoid_util]
Monoid.M [in Algebra.Abelian_group_facts]
P
Part_set_greater.invX [in Algebra.Parts]Part_set_greater.X [in Algebra.Parts]
Part_set_greater.X_def [in Algebra.Parts]
Part_set_greater.fsurj [in Algebra.Parts]
Part_set_greater.f [in Algebra.Parts]
Part_set_greater.E [in Algebra.Parts]
Part_set.eq_part_equiv [in Algebra.Parts]
Part_set.E [in Algebra.Parts]
Part_type.P [in Algebra.Parts]
Part_type.E [in Algebra.Parts]
Projections.E [in Algebra.Cartesian]
Projections.F [in Algebra.Cartesian]
R
Restrictions1.E [in Algebra.Parts3]Restrictions1.f [in Algebra.Parts3]
Restrictions1.F [in Algebra.Parts3]
Ring_algebra_as_ring.A [in Algebra.Algebra_facts]
Ring_algebra_as_ring.R [in Algebra.Algebra_facts]
Ring_as_module.R [in Algebra.Ideal]
Ring.E [in Algebra.Ring_util]
Ring.oppcomp [in Algebra.Ring_util]
Ring.ringdistl [in Algebra.Ring_util]
Ring.ringdistr [in Algebra.Ring_util]
Ring.ringmult [in Algebra.Ring_util]
Ring.ringmultassoc [in Algebra.Ring_util]
Ring.ringmultcomp [in Algebra.Ring_util]
Ring.ringopp [in Algebra.Ring_util]
Ring.ringoppr [in Algebra.Ring_util]
Ring.ringplus [in Algebra.Ring_util]
Ring.ringplusassoc [in Algebra.Ring_util]
Ring.ringpluscom [in Algebra.Ring_util]
Ring.ringpluscomp [in Algebra.Ring_util]
Ring.un [in Algebra.Ring_util]
Ring.ununitlringmult [in Algebra.Ring_util]
Ring.ununitringmultr [in Algebra.Ring_util]
Ring.zero [in Algebra.Ring_util]
Ring.zerounitringplusr [in Algebra.Ring_util]
S
Sets1.eqT_equiv [in Algebra.Sets]Sets1.Maps1.Maps1_3.f [in Algebra.Sets]
Sets1.Maps1.Maps1_3.g [in Algebra.Sets]
Sets1.Maps1.Maps1_3.G [in Algebra.Sets]
Sets1.Maps1.Maps1_3.F [in Algebra.Sets]
Sets1.Maps1.Maps1_3.E [in Algebra.Sets]
Sets1.Maps1.Maps1_2.B [in Algebra.Sets]
Sets1.Maps1.Maps1_2.A [in Algebra.Sets]
Sets1.Maps1.Maps1_1.Map_eq_equiv [in Algebra.Sets]
Sets1.Maps1.Maps1_1.B [in Algebra.Sets]
Sets1.Maps1.Maps1_1.A [in Algebra.Sets]
Sets1.Quotient1.E [in Algebra.Sets]
Sets1.Quotient1.R [in Algebra.Sets]
Sets1.Quotient1.R_equiv [in Algebra.Sets]
Sets1.Relations.E [in Algebra.Sets]
Sgroup.S [in Algebra.Abelian_group_facts]
Single1.E [in Algebra.Singleton]
Subcategory_def.CompC'_ok [in Algebra.Subcat]
Subcategory_def.idC'ok [in Algebra.Subcat]
Subcategory_def.idC' [in Algebra.Subcat]
Subcategory_def.CompC' [in Algebra.Subcat]
Subcategory_def.homC' [in Algebra.Subcat]
Subcategory_def.i [in Algebra.Subcat]
Subcategory_def.C' [in Algebra.Subcat]
Subcategory_def.C [in Algebra.Subcat]
Subtype.E [in Algebra.Parts]
Subtype.F [in Algebra.Parts]
Subtype.i [in Algebra.Parts]
T
tiroirs_def.f [in Algebra.Tiroirs]tiroirs_def.F [in Algebra.Tiroirs]
tiroirs_def.E [in Algebra.Tiroirs]
U
Union_of_part.P [in Algebra.Parts]Union_of_part.E [in Algebra.Parts]
Union1.E [in Algebra.Union]
Unit.e [in Algebra.Monoid_cat]
Unit.E [in Algebra.Monoid_cat]
Unit.f [in Algebra.Monoid_cat]
Z
Zup1.G [in Algebra.Z_group]Zup1.R [in Algebra.ZUP]
Zup1.r [in Algebra.Z_group]
Zup2.G [in Algebra.Z_group]
Zup2.pos_def.r [in Algebra.Z_group]
Zup2.r [in Algebra.Z_group]
Library Index
A
Abelian_group_catAbelian_group_facts
Algebra
Algebra_facts
C
Cantor_BernsteinCartesian
Categories
Categories2
Cfield_cat
Cfield_facts
Complex_field
D
DiffE
Endo_setF
Field_catField_facts
Fmap
Fpart
Fpart2
Fraction_field
Free_group
Free_abelian_group
Free_monoid
Free_module
Free_abelian_monoid
G
Generated_moduleGenerated_group
Generated_monoid
Group_hom_factor
Group_of_group_hom
Group_kernel
Group_power
Group_cat
Group_facts
Group_util
Group_quotient
H
Hom_moduleI
IdealIntegral_domain_cat
Integral_domain_facts
Inter
M
Module_utilModule_cat
Module_facts
Module_kernel
Monoid_cat
Monoid_facts
Monoid_util
Monoid_kernel
O
Operation_of_monoidP
PartsParts2
Parts3
Q
QfieldR
Ring_catRing_facts
Ring_util
S
SetsSet_cat
Sgroup_facts
Sgroup_cat
Singleton
Subcat
Sub_module
Sub_monoid
Sub_sgroup
Sub_group
T
TiroirsU
UnionZ
ZringZUP
Z_group
Z_group_facts
Lemma Index
A
ABELIAN_GROUP4 [in Algebra.Abelian_group_facts]ABELIAN_GROUP_permute [in Algebra.Abelian_group_facts]
ABELIAN_GROUP_com [in Algebra.Abelian_group_facts]
ABELIAN_MONOID4 [in Algebra.Abelian_group_facts]
ABELIAN_MONOID_permute [in Algebra.Abelian_group_facts]
ABELIAN_MONOID_com [in Algebra.Abelian_group_facts]
ABELIAN_SGROUP4 [in Algebra.Abelian_group_facts]
ABELIAN_SGROUP_permute [in Algebra.Abelian_group_facts]
ABELIAN_SGROUP_com [in Algebra.Abelian_group_facts]
addfraction_law [in Algebra.Fraction_field]
addfraction_law_r [in Algebra.Fraction_field]
addfraction_fun_com [in Algebra.Fraction_field]
addfraction_law_l [in Algebra.Fraction_field]
add_minus [in Algebra.Fpart]
add_part_simpl [in Algebra.Fpart]
add_part_in_el_not_in [in Algebra.Fpart]
add_part_in_el_diff [in Algebra.Fpart]
add_in [in Algebra.Fpart]
add_part_com [in Algebra.Fpart]
add_part_in [in Algebra.Fpart]
add_part_comp [in Algebra.Fpart]
ALGEBRA_mult_lin_right [in Algebra.Algebra_facts]
ALGEBRA_lin_right [in Algebra.Algebra_facts]
ALGEBRA_comp [in Algebra.Algebra_facts]
Ap_comp [in Algebra.Sets]
ax1 [in Algebra.Z_group]
ax2 [in Algebra.Z_group]
ax3 [in Algebra.Z_group]
ax4 [in Algebra.Z_group]
ax5 [in Algebra.Z_group]
ax6 [in Algebra.Z_group]
ax7 [in Algebra.Z_group]
ax8 [in Algebra.Z_group]
B
bijective_surjective [in Algebra.Sets]bijective_injective [in Algebra.Sets]
bijective_comp [in Algebra.Sets]
bij_group_quo_ker_coKer_bijective [in Algebra.Group_hom_factor]
Build_Ctype_comp2 [in Algebra.Complex_field]
Build_Ctype_comp [in Algebra.Complex_field]
C
Cantor_Berstein [in Algebra.Cantor_Bernstein]cardinalO_unique [in Algebra.Fpart]
cardinal_minus_part [in Algebra.Tiroirs]
cardinal_union_inter [in Algebra.Fpart2]
cardinal_diff [in Algebra.Fpart2]
cardinal_union [in Algebra.Fpart2]
cardinal_union_disjoint [in Algebra.Fpart2]
cardinal_unique [in Algebra.Fpart]
cardinal_S [in Algebra.Fpart]
cardinal_ind2 [in Algebra.Fpart]
cardinal_sup3 [in Algebra.Fpart]
cardinal_1_single [in Algebra.Fpart]
cardinal_O_empty [in Algebra.Fpart]
cardinal_pair [in Algebra.Fpart]
cardinal_single [in Algebra.Fpart]
cardinal_empty_O [in Algebra.Fpart]
cardinal_comp_r [in Algebra.Fpart]
cardinal_comp_l [in Algebra.Fpart]
cardinal_comp [in Algebra.Fpart]
cardinal_included [in Algebra.Fmap]
cardinal_image_equal_injective [in Algebra.Fmap]
cardinal_image_strict_lesser [in Algebra.Fmap]
cardinal_image_injective [in Algebra.Fmap]
cardinal_image_lesser [in Algebra.Fmap]
cart_eq_equiv [in Algebra.Cartesian]
CFIELD_mult_div_r [in Algebra.Cfield_facts]
CFIELD_mult3bis [in Algebra.Cfield_facts]
CFIELD_mult3 [in Algebra.Cfield_facts]
CFIELD_mult4 [in Algebra.Cfield_facts]
CFIELD_simpl_l [in Algebra.Cfield_facts]
CFIELD_inverse_law2 [in Algebra.Cfield_facts]
CFIELD_com [in Algebra.Cfield_facts]
coKer_prop [in Algebra.Group_kernel]
coKer_prop [in Algebra.Module_kernel]
compl_not_compl [in Algebra.Parts2]
compl_included [in Algebra.Parts2]
compl_not_in [in Algebra.Parts2]
compl_compl [in Algebra.Parts2]
compl_comp_rev [in Algebra.Parts2]
compl_comp [in Algebra.Parts2]
compl_in [in Algebra.Parts2]
comp_hom_unit_r [in Algebra.Categories]
comp_hom_unit_l [in Algebra.Categories]
comp_hom_assoc [in Algebra.Categories]
comp_hom_compatible [in Algebra.Categories]
comp_is_id_then_surjective [in Algebra.Sets]
comp_is_id_then_injective [in Algebra.Sets]
comp_is_id_then_bijective [in Algebra.Sets]
comp_surjective [in Algebra.Sets]
comp_injective [in Algebra.Sets]
comp_map_assoc [in Algebra.Sets]
comp_map_comp [in Algebra.Sets]
comp_map_fun_compatible [in Algebra.Sets]
comp_map_map_compatible [in Algebra.Set_cat]
couple_comp [in Algebra.Cartesian]
coupl_proj [in Algebra.Cartesian]
CRING_mult3bis [in Algebra.Ring_facts]
CRING_mult3 [in Algebra.Ring_facts]
CRING_mult4 [in Algebra.Ring_facts]
CRING_com [in Algebra.Ring_facts]
C_inv_r [in Algebra.Complex_field]
D
diff_comp [in Algebra.Diff]diff_add_part2 [in Algebra.Tiroirs]
diff_add_part_not_in [in Algebra.Fpart2]
diff_not_in [in Algebra.Fpart2]
diff_add_part [in Algebra.Fpart2]
diff_in_r [in Algebra.Fpart2]
diff_in_l [in Algebra.Fpart2]
disjoint_diff [in Algebra.Fpart2]
disjoint_not_in_r [in Algebra.Fpart2]
disjoint_inclus [in Algebra.Fpart2]
disjoint_comp [in Algebra.Fpart2]
E
empty_included [in Algebra.Parts]empty_prop [in Algebra.Parts]
empty_inter [in Algebra.Fpart2]
empty_diff [in Algebra.Fpart2]
empty_not_in [in Algebra.Fpart2]
eqFaG_Equiv [in Algebra.Free_abelian_group]
eqFaM_Equiv [in Algebra.Free_abelian_monoid]
eqFG_Equiv [in Algebra.Free_group]
eqFMd_Equiv [in Algebra.Free_module]
eqFM_Equiv [in Algebra.Free_monoid]
eqfraction_trans [in Algebra.Fraction_field]
eqfraction_sym [in Algebra.Fraction_field]
eqfraction_num0 [in Algebra.Fraction_field]
eqfraction_refl [in Algebra.Fraction_field]
eqfraction0 [in Algebra.Fraction_field]
equiv_trans [in Algebra.Sets]
equiv_sym [in Algebra.Sets]
equiv_refl [in Algebra.Sets]
eq_part_included [in Algebra.Parts]
eunitgenlawl [in Algebra.Group_util]
eunitl [in Algebra.Group_util]
eunitl [in Algebra.Monoid_util]
eunitr [in Algebra.Group_util]
eunitr [in Algebra.Monoid_util]
F
factor_group_hom [in Algebra.Group_hom_factor]FaG_comp_prop [in Algebra.Free_abelian_group]
FaM_comp_prop [in Algebra.Free_abelian_monoid]
fassoc [in Algebra.Group_util]
fassoc [in Algebra.Monoid_util]
FG_comp_prop [in Algebra.Free_group]
FIELD_inv_div [in Algebra.Field_facts]
FIELD_div_div2 [in Algebra.Field_facts]
FIELD_mult_div_l [in Algebra.Field_facts]
FIELD_div_div [in Algebra.Field_facts]
FIELD_one_div_div [in Algebra.Field_facts]
FIELD_one_div_xy [in Algebra.Field_facts]
FIELD_one_div_x [in Algebra.Field_facts]
FIELD_simpl_r [in Algebra.Field_facts]
FIELD_x_div_x [in Algebra.Field_facts]
FIELD_inverse_law [in Algebra.Field_facts]
FIELD_law_inverse [in Algebra.Field_facts]
FIELD_integral_domain_r [in Algebra.Field_facts]
FIELD_integral_domain_l [in Algebra.Field_facts]
FIELD_inverse_inverse [in Algebra.Field_facts]
FIELD_inverse_non_zero [in Algebra.Field_facts]
FIELD_reg_right [in Algebra.Field_facts]
FIELD_reg_left [in Algebra.Field_facts]
FIELD_unit_inverse [in Algebra.Field_facts]
FIELD_comp [in Algebra.Field_facts]
FIELD_unit_non_zero [in Algebra.Field_facts]
FIELD_inverse_l [in Algebra.Field_facts]
FIELD_inverse_r [in Algebra.Field_facts]
finite_surjective_injective [in Algebra.Fmap]
finite_injective_surjective [in Algebra.Fmap]
FMd_comp_prop [in Algebra.Free_module]
FM_comp_prop [in Algebra.Free_monoid]
full_included [in Algebra.Parts]
full_set_full [in Algebra.Parts]
full_prop [in Algebra.Parts]
G
generated_monoid_prop_rev [in Algebra.Generated_monoid]generated_monoid_prop [in Algebra.Generated_monoid]
generated_monoid_prop_included [in Algebra.Generated_monoid]
generated_monoid_minimal [in Algebra.Generated_monoid]
generated_group_prop_rev [in Algebra.Generated_group]
generated_group_prop [in Algebra.Generated_group]
generated_group_prop_included [in Algebra.Generated_group]
generated_group_minimal [in Algebra.Generated_group]
generated_ideal_minimal [in Algebra.Ideal]
generated_ideal_included [in Algebra.Ideal]
generated_module_prop_rev [in Algebra.Generated_module]
generated_module_prop [in Algebra.Generated_module]
generated_module_prop_included [in Algebra.Generated_module]
generated_module_minimal [in Algebra.Generated_module]
geninvl [in Algebra.Group_util]
GROUP_hom_prop [in Algebra.Group_facts]
GROUP_inverse_law [in Algebra.Group_facts]
GROUP_law_inverse [in Algebra.Group_facts]
GROUP_inverse_inverse [in Algebra.Group_facts]
GROUP_reg_right [in Algebra.Group_facts]
GROUP_reg_left [in Algebra.Group_facts]
GROUP_unit_inverse [in Algebra.Group_facts]
GROUP_inverse_l [in Algebra.Group_facts]
GROUP_inverse_r [in Algebra.Group_facts]
GROUP_comp [in Algebra.Group_facts]
group_power_mult [in Algebra.Z_group_facts]
group_power_inv [in Algebra.Z_group_facts]
group_power_1 [in Algebra.Z_group_facts]
group_power_0 [in Algebra.Z_group_facts]
group_power_S [in Algebra.Z_group_facts]
group_power_plus [in Algebra.Z_group_facts]
group_quo_eqrel_equiv [in Algebra.Group_quotient]
group_hom_inv_prop [in Algebra.Group_of_group_hom]
group_hom_unit_prop [in Algebra.Group_of_group_hom]
group_hom_law_prop [in Algebra.Group_of_group_hom]
group_power_zero [in Algebra.Group_power]
I
ideal_prop4 [in Algebra.Ideal]ideal_prop3 [in Algebra.Ideal]
ideal_prop2 [in Algebra.Ideal]
ideal_prop [in Algebra.Ideal]
Id_is_bijective [in Algebra.Sets]
Id_unit_l [in Algebra.Sets]
Id_unit_r [in Algebra.Sets]
id_map_parts_equal_prop [in Algebra.Parts]
image_in_image [in Algebra.Parts2]
image_comp [in Algebra.Parts2]
image_included [in Algebra.Parts2]
image_in [in Algebra.Parts2]
image_invimage_image [in Algebra.Parts3]
image_invimage [in Algebra.Parts3]
image_monoid_prop_rev [in Algebra.Monoid_kernel]
image_monoid_prop [in Algebra.Monoid_kernel]
imag_comp [in Algebra.Complex_field]
included_comp [in Algebra.Parts]
included_trans [in Algebra.Parts]
included_antisym [in Algebra.Parts]
included_refl [in Algebra.Parts]
included_inter_r [in Algebra.Inter]
included_inter_l [in Algebra.Inter]
included_add_part [in Algebra.Fpart2]
included_union_r [in Algebra.Union]
included_union_l [in Algebra.Union]
included2_inter [in Algebra.Inter]
included2_union [in Algebra.Union]
injective_comp [in Algebra.Sets]
inj_submodule_injective [in Algebra.Sub_module]
inj_subgroup_injective [in Algebra.Sub_group]
inj_part_included_injective [in Algebra.Parts]
inj_part_included_prop [in Algebra.Parts]
inj_part_injective [in Algebra.Parts]
inj_coKer_group_injective [in Algebra.Group_hom_factor]
inj_subgroup_injective [in Algebra.Sub_sgroup]
inj_subsmonoid_injective [in Algebra.Sub_monoid]
INTEGRAL_DOMAIN_mult_eq_l [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_eq_r [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_simpl_l [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_simpl_r [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_n0_l [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_n0_r [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_r [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_mult_l [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_prop [in Algebra.Integral_domain_facts]
INTEGRAL_DOMAIN_prop_rev [in Algebra.Integral_domain_facts]
inter_com [in Algebra.Inter]
inter_assoc [in Algebra.Inter]
inter_comp [in Algebra.Inter]
inter_not_in_r [in Algebra.Inter]
inter_not_in_l [in Algebra.Inter]
inter_add_part_not_in [in Algebra.Fpart2]
inter_add_part [in Algebra.Fpart2]
inter_not_in [in Algebra.Fpart2]
invimage_image_invimage [in Algebra.Parts3]
invimage_image [in Algebra.Parts3]
invimage_comp [in Algebra.Parts3]
invimage_included [in Algebra.Parts3]
invimage_in [in Algebra.Parts3]
invl [in Algebra.Group_util]
invr [in Algebra.Group_util]
in_image [in Algebra.Parts2]
in_compl [in Algebra.Parts2]
in_part_comp_r [in Algebra.Parts]
in_part_comp_l [in Algebra.Parts]
in_part_inter [in Algebra.Inter]
in_part_inter_r [in Algebra.Inter]
in_part_inter_l [in Algebra.Inter]
in_part_trans_eq [in Algebra.Fpart2]
in_diff [in Algebra.Fpart2]
in_eq_part [in Algebra.Fpart2]
in_invimage [in Algebra.Parts3]
in_single [in Algebra.Singleton]
in_part_union [in Algebra.Union]
in_part_union_r [in Algebra.Union]
in_part_union_l [in Algebra.Union]
K
kernel_normal [in Algebra.Group_kernel]Ker_prop_rev [in Algebra.Group_kernel]
Ker_prop [in Algebra.Group_kernel]
Ker_prop_rev [in Algebra.Module_kernel]
Ker_prop [in Algebra.Module_kernel]
L
Leibnitz_set_prop_rev [in Algebra.Sets]Leibnitz_set_prop [in Algebra.Sets]
M
map_ext [in Algebra.Sets]map_couple_proj_prop [in Algebra.Cartesian]
map_not_injective [in Algebra.Fmap]
minus_add [in Algebra.Fpart]
minus_trans_not_in [in Algebra.Fpart]
minus_not_in [in Algebra.Fpart]
minus_part_com [in Algebra.Fpart]
minus_part_not_in [in Algebra.Fpart]
minus_part_comp [in Algebra.Fpart]
MODULE_hom_prop [in Algebra.Module_facts]
MODULE_mult_op_l [in Algebra.Module_facts]
MODULE_mult_op_r [in Algebra.Module_facts]
MODULE_absorbant_r [in Algebra.Module_facts]
MODULE_absorbant_l [in Algebra.Module_facts]
MODULE_unit_l [in Algebra.Module_facts]
MODULE_dist_l [in Algebra.Module_facts]
MODULE_dist_r [in Algebra.Module_facts]
MODULE_assoc [in Algebra.Module_facts]
MODULE_comp [in Algebra.Module_facts]
MONOID_hom_prop [in Algebra.Monoid_facts]
MONOID_unit_unique [in Algebra.Monoid_facts]
MONOID_unit_l [in Algebra.Monoid_facts]
MONOID_unit_r [in Algebra.Monoid_facts]
multfraction_com [in Algebra.Fraction_field]
multfraction_dist_l [in Algebra.Fraction_field]
N
nat_to_group_unit [in Algebra.Z_group_facts]nat_to_group_mult [in Algebra.Z_group_facts]
nat_to_group_comp [in Algebra.Z_group_facts]
nat_to_group_mult [in Algebra.ZUP]
nat_to_group_inverse [in Algebra.Z_group]
nat_to_group_com4 [in Algebra.Z_group]
nat_to_group_com3 [in Algebra.Z_group]
nat_to_group_minus [in Algebra.Z_group]
nat_to_group_com2 [in Algebra.Z_group]
nat_to_group_add [in Algebra.Z_group]
nat_to_group_com [in Algebra.Z_group]
normal_com_in [in Algebra.Group_quotient]
not_in_compl [in Algebra.Parts2]
not_in_comp_r [in Algebra.Parts2]
not_in_comp_l [in Algebra.Parts2]
not_inpart_comp_r [in Algebra.Parts]
not_in_part_trans_eq [in Algebra.Fpart]
not_in_part_trans [in Algebra.Fpart]
not_in_empty [in Algebra.Fpart]
not_included_exist [in Algebra.Fmap]
not_surjective_prop [in Algebra.Fmap]
not_injective_prop [in Algebra.Fmap]
O
operation_unit [in Algebra.Operation_of_monoid]operation_assoc [in Algebra.Operation_of_monoid]
P
part_set_is_strictly_greater_than_set [in Algebra.Parts]part_set_is_strictly_greater_than_set1 [in Algebra.Parts]
pos_abs_comp [in Algebra.Z_group_facts]
pos_nat_group [in Algebra.Z_group]
pos_abs_ok [in Algebra.Z_group]
proj1_comp [in Algebra.Cartesian]
proj2_comp [in Algebra.Cartesian]
R
real_comp [in Algebra.Complex_field]Refl [in Algebra.Sets]
Rel_comp [in Algebra.Sets]
restrict_prop_in_part [in Algebra.Parts3]
restrict_prop [in Algebra.Parts3]
RING_ALGEBRA_unit_r [in Algebra.Algebra_facts]
RING_ALGEBRA_unit_l [in Algebra.Algebra_facts]
RING_ALGEBRA_assoc [in Algebra.Algebra_facts]
RING_hom_ext [in Algebra.Ring_facts]
RING_one_prop [in Algebra.Ring_facts]
RING_hom_prop [in Algebra.Ring_facts]
RING_op_mult_r [in Algebra.Ring_facts]
RING_op_mult_l [in Algebra.Ring_facts]
RING_absorbant_l [in Algebra.Ring_facts]
RING_absorbant_r [in Algebra.Ring_facts]
RING_dist_l [in Algebra.Ring_facts]
RING_dist_r [in Algebra.Ring_facts]
RING_unit_l [in Algebra.Ring_facts]
RING_unit_r [in Algebra.Ring_facts]
RING_comp [in Algebra.Ring_facts]
RING_assoc [in Algebra.Ring_facts]
S
set_full_set [in Algebra.Parts]sgroup_powers_rev [in Algebra.Z_group]
sgroup_powers_prop [in Algebra.Z_group]
SGROUP_hom_prop [in Algebra.Sgroup_facts]
SGROUP_comp [in Algebra.Sgroup_facts]
SGROUP_assoc [in Algebra.Sgroup_facts]
single_add [in Algebra.Fpart]
single_simpl [in Algebra.Singleton]
single_prop_rev [in Algebra.Singleton]
single_prop [in Algebra.Singleton]
single_law [in Algebra.Singleton]
subgroup_in_prop [in Algebra.Sub_group]
submodule_in_prop [in Algebra.Sub_module]
submonoid_in_prop [in Algebra.Sub_monoid]
subsgroup_in_prop [in Algebra.Sub_sgroup]
subtype_image_equiv [in Algebra.Parts]
surjective_comp [in Algebra.Sets]
surj_part_image_surjective [in Algebra.Parts2]
surj_set_image_surjective [in Algebra.Parts2]
surj_set_quo_surjective [in Algebra.Sets]
surj_group_quo_ker_surjective [in Algebra.Group_hom_factor]
Sym [in Algebra.Sets]
T
tiroirs [in Algebra.Tiroirs]Trans [in Algebra.Sets]
U
union_part_upper_bound [in Algebra.Parts]union_part_included [in Algebra.Parts]
union_part_prop_rev [in Algebra.Parts]
union_part_prop [in Algebra.Parts]
union_diff [in Algebra.Fpart2]
union_not_in [in Algebra.Fpart2]
union_unit_l [in Algebra.Fpart]
union_com [in Algebra.Union]
union_assoc [in Algebra.Union]
union_comp [in Algebra.Union]
union_not_in_l [in Algebra.Union]
Z
Zlemma1 [in Algebra.Z_group]Zlt_reg_l [in Algebra.Z_group]
Zl1 [in Algebra.Z_group]
Zl2 [in Algebra.Z_group]
Zl3 [in Algebra.Z_group]
Zl4 [in Algebra.Z_group]
Zl5 [in Algebra.Z_group]
Zopp1 [in Algebra.Z_group_facts]
Zopp2 [in Algebra.Z_group_facts]
Z_group_nat_fun_mult_pos [in Algebra.Z_group_facts]
Z_to_group_nat_unit [in Algebra.Z_group_facts]
Z_to_group_nat_inv [in Algebra.Z_group_facts]
Z_to_group_nat_neg [in Algebra.Z_group_facts]
Z_to_group_nat_fun_comp [in Algebra.Z_group_facts]
Z_to_group_nat_eq_pos [in Algebra.Z_group_facts]
Z_one_diff_zero [in Algebra.Qfield]
Z_to_group_fun_eq [in Algebra.Z_group]
Constructor Index
C
cardinal_add [in Algebra.Fpart]cardinal_empty [in Algebra.Fpart]
E
eqFaG_com [in Algebra.Free_abelian_group]eqFaG_trans [in Algebra.Free_abelian_group]
eqFaG_sym [in Algebra.Free_abelian_group]
eqFaG_refl [in Algebra.Free_abelian_group]
eqFaG_invr [in Algebra.Free_abelian_group]
eqFaG_inv [in Algebra.Free_abelian_group]
eqFaG_law0r [in Algebra.Free_abelian_group]
eqFaG_law_assoc [in Algebra.Free_abelian_group]
eqFaG_law [in Algebra.Free_abelian_group]
eqFaG_Var [in Algebra.Free_abelian_group]
eqFaM_com [in Algebra.Free_abelian_monoid]
eqFaM_trans [in Algebra.Free_abelian_monoid]
eqFaM_sym [in Algebra.Free_abelian_monoid]
eqFaM_refl [in Algebra.Free_abelian_monoid]
eqFaM_law0l [in Algebra.Free_abelian_monoid]
eqFaM_law0r [in Algebra.Free_abelian_monoid]
eqFaM_law_assoc [in Algebra.Free_abelian_monoid]
eqFaM_law [in Algebra.Free_abelian_monoid]
eqFaM_Var [in Algebra.Free_abelian_monoid]
eqFG_trans [in Algebra.Free_group]
eqFG_sym [in Algebra.Free_group]
eqFG_refl [in Algebra.Free_group]
eqFG_invr [in Algebra.Free_group]
eqFG_inv [in Algebra.Free_group]
eqFG_law0r [in Algebra.Free_group]
eqFG_law_assoc [in Algebra.Free_group]
eqFG_law [in Algebra.Free_group]
eqFG_Var [in Algebra.Free_group]
eqFMd_op_unit [in Algebra.Free_module]
eqFMd_op_assoc [in Algebra.Free_module]
eqFMd_oplin_r [in Algebra.Free_module]
eqFMd_oplin_l [in Algebra.Free_module]
eqFMd_op_comp [in Algebra.Free_module]
eqFMd_com [in Algebra.Free_module]
eqFMd_trans [in Algebra.Free_module]
eqFMd_sym [in Algebra.Free_module]
eqFMd_refl [in Algebra.Free_module]
eqFMd_invr [in Algebra.Free_module]
eqFMd_inv [in Algebra.Free_module]
eqFMd_law0r [in Algebra.Free_module]
eqFMd_law_assoc [in Algebra.Free_module]
eqFMd_law [in Algebra.Free_module]
eqFMd_Var [in Algebra.Free_module]
eqFM_trans [in Algebra.Free_monoid]
eqFM_sym [in Algebra.Free_monoid]
eqFM_refl [in Algebra.Free_monoid]
eqFM_law0l [in Algebra.Free_monoid]
eqFM_law0r [in Algebra.Free_monoid]
eqFM_law_assoc [in Algebra.Free_monoid]
eqFM_law [in Algebra.Free_monoid]
eqFM_Var [in Algebra.Free_monoid]
I
Inv [in Algebra.Free_group]Inv [in Algebra.Free_module]
Inv [in Algebra.Free_abelian_group]
L
Law [in Algebra.Free_monoid]Law [in Algebra.Free_group]
Law [in Algebra.Free_abelian_monoid]
Law [in Algebra.Free_module]
Law [in Algebra.Free_abelian_group]
O
Op [in Algebra.Free_module]U
Unit [in Algebra.Free_monoid]Unit [in Algebra.Free_group]
Unit [in Algebra.Free_abelian_monoid]
Unit [in Algebra.Free_module]
Unit [in Algebra.Free_abelian_group]
V
Var [in Algebra.Free_monoid]Var [in Algebra.Free_group]
Var [in Algebra.Free_abelian_monoid]
Var [in Algebra.Free_module]
Var [in Algebra.Free_abelian_group]
Axiom Index
A
ALGEBRA_mult_lin_left [in Algebra.Algebra_facts]ALGEBRA_lin_left [in Algebra.Algebra_facts]
C
cardinal_equal_included_equal [in Algebra.Fmap]D
diff_el_union_single [in Algebra.Fmap]diff_single_not_in [in Algebra.Fmap]
G
group_power_S [in Algebra.Group_power]I
image_full_surjective [in Algebra.Fmap]image_single [in Algebra.Fmap]
image_union [in Algebra.Fmap]
image_empty [in Algebra.Fmap]
inter_union_dist_l [in Algebra.Inter]
inter_union_dist_r [in Algebra.Inter]
in_part_union_or [in Algebra.Union]
N
not_in_part_comp_r [in Algebra.Fmap]S
surjective_image_full [in Algebra.Fmap]U
union_single_in [in Algebra.Fmap]union_empty_r [in Algebra.Union]
union_empty_l [in Algebra.Union]
Inductive Index
C
cardinal [in Algebra.Fpart]E
eqFaG [in Algebra.Free_abelian_group]eqFaM [in Algebra.Free_abelian_monoid]
eqFG [in Algebra.Free_group]
eqFM [in Algebra.Free_monoid]
eqFMd [in Algebra.Free_module]
F
FaG [in Algebra.Free_abelian_group]FaM [in Algebra.Free_abelian_monoid]
FG [in Algebra.Free_group]
FM [in Algebra.Free_monoid]
FMd [in Algebra.Free_module]
Projection Index
A
abelian_group_on_def [in Algebra.Abelian_group_cat]abelian_group_group [in Algebra.Abelian_group_cat]
abelian_group_abelian_monoid [in Algebra.Abelian_group_cat]
abelian_monoid_on_def [in Algebra.Abelian_group_cat]
abelian_monoid_monoid [in Algebra.Abelian_group_cat]
abelian_monoid_abelian_sgroup [in Algebra.Abelian_group_cat]
abelian_sgroup_on_def [in Algebra.Abelian_group_cat]
abelian_sgroup_sgroup [in Algebra.Abelian_group_cat]
abelian_sgroup_com_prf [in Algebra.Abelian_group_cat]
algebra_on_def [in Algebra.Algebra]
algebra_carrier [in Algebra.Algebra]
algebra_bilinear_map [in Algebra.Algebra]
Ap [in Algebra.Sets]
C
Carrier [in Algebra.Sets]cart_r [in Algebra.Cartesian]
cart_l [in Algebra.Cartesian]
Cdistrib_prf [in Algebra.Categories2]
Cfctr_morph [in Algebra.Categories2]
Cfctr_ob [in Algebra.Categories2]
cfield_on_def [in Algebra.Cfield_cat]
cfield_ring [in Algebra.Cfield_cat]
Cim_of_id_prf [in Algebra.Categories2]
cring_on_def [in Algebra.Ring_cat]
cring_ring [in Algebra.Ring_cat]
cring_com_prf [in Algebra.Ring_cat]
D
den [in Algebra.Fraction_field]den_prf [in Algebra.Fraction_field]
distrib_prf [in Algebra.Categories2]
E
Equal [in Algebra.Sets]F
fctr_morph [in Algebra.Categories2]fctr_ob [in Algebra.Categories2]
field_on_def [in Algebra.Field_cat]
field_ring [in Algebra.Field_cat]
field_unit_non_zero [in Algebra.Field_cat]
field_inverse_l_prf [in Algebra.Field_cat]
field_inverse_r_prf [in Algebra.Field_cat]
field_inverse_map [in Algebra.Field_cat]
G
group_on_def [in Algebra.Group_cat]group_monoid [in Algebra.Group_cat]
group_inverse_l_prf [in Algebra.Group_cat]
group_inverse_r_prf [in Algebra.Group_cat]
group_inverse_map [in Algebra.Group_cat]
H
Hom [in Algebra.Categories]Hom_comp_unit_r_prf [in Algebra.Categories]
Hom_comp_unit_l_prf [in Algebra.Categories]
Hom_comp_assoc_prf [in Algebra.Categories]
Hom_id [in Algebra.Categories]
Hom_comp [in Algebra.Categories]
I
ideal_prf [in Algebra.Ideal]ideal_subgroup [in Algebra.Ideal]
idomain_on_def [in Algebra.Integral_domain_cat]
idomain_ring [in Algebra.Integral_domain_cat]
idomain_prf [in Algebra.Integral_domain_cat]
imag [in Algebra.Complex_field]
im_of_id_prf [in Algebra.Categories2]
M
Map_compatible_prf [in Algebra.Sets]module_hom_prf [in Algebra.Module_cat]
module_monoid_hom [in Algebra.Module_cat]
module_on_def [in Algebra.Module_cat]
module_carrier [in Algebra.Module_cat]
module_op_lin_right_prf [in Algebra.Module_cat]
module_op_lin_left_prf [in Algebra.Module_cat]
module_op [in Algebra.Module_cat]
monoid_hom_prf [in Algebra.Monoid_cat]
monoid_sgroup_hom [in Algebra.Monoid_cat]
monoid_on_def [in Algebra.Monoid_cat]
monoid_sgroup [in Algebra.Monoid_cat]
monoid_unit_l_prf [in Algebra.Monoid_cat]
monoid_unit_r_prf [in Algebra.Monoid_cat]
monoid_unit [in Algebra.Monoid_cat]
N
num [in Algebra.Fraction_field]O
Ob [in Algebra.Categories]P
Pred_compatible_prf [in Algebra.Parts]Pred_fun [in Algebra.Parts]
Prf_equiv [in Algebra.Sets]
R
real [in Algebra.Complex_field]Rel_compatible_prf [in Algebra.Sets]
Rel_fun [in Algebra.Sets]
ring_algebra_on_def [in Algebra.Algebra]
ring_algebra_algebra [in Algebra.Algebra]
ring_algebra_unit_r [in Algebra.Algebra]
ring_algebra_unit_l [in Algebra.Algebra]
ring_algebra_unit [in Algebra.Algebra]
ring_algebra_assoc [in Algebra.Algebra]
ring_mult_hom_prf [in Algebra.Ring_cat]
ring_mult_hom_unit [in Algebra.Ring_cat]
ring_plus_hom [in Algebra.Ring_cat]
ring_on_def [in Algebra.Ring_cat]
ring_group [in Algebra.Ring_cat]
ring_dist_l_prf [in Algebra.Ring_cat]
ring_dist_r_prf [in Algebra.Ring_cat]
ring_monoid [in Algebra.Ring_cat]
ring_mult_monoid [in Algebra.Ring_cat]
ring_mult_sgroup [in Algebra.Ring_cat]
S
sgroup_hom_prf [in Algebra.Sgroup_cat]sgroup_map [in Algebra.Sgroup_cat]
sgroup_on_def [in Algebra.Sgroup_cat]
sgroup_set [in Algebra.Sgroup_cat]
sgroup_assoc_prf [in Algebra.Sgroup_cat]
sgroup_law_map [in Algebra.Sgroup_cat]
subgroup_prop [in Algebra.Sub_group]
subgroup_submonoid [in Algebra.Sub_group]
submodule_prop [in Algebra.Sub_module]
submodule_subgroup [in Algebra.Sub_module]
submonoid_prop [in Algebra.Sub_monoid]
submonoid_subsgroup [in Algebra.Sub_monoid]
subsgroup_prop [in Algebra.Sub_sgroup]
subsgroup_part [in Algebra.Sub_sgroup]
subtype_prf [in Algebra.Parts]
subtype_elt [in Algebra.Parts]
subtype_image_inj [in Algebra.Parts]
subtype_image_carrier [in Algebra.Parts]
Section Index
A
Abelian_group [in Algebra.Group_util]Abelian_monoid [in Algebra.Monoid_util]
algebra_def [in Algebra.Algebra]
B
Build_sub_group [in Algebra.Group_util]Build_sub_monoid [in Algebra.Monoid_util]
C
Cantor_Bernstein [in Algebra.Cantor_Bernstein]Category_def.Full_subcat_def [in Algebra.Categories]
Category_def.Category_comp [in Algebra.Categories]
Category_def.Category_def1 [in Algebra.Categories]
Category_def [in Algebra.Categories]
Commutative_rings [in Algebra.Ring_facts]
Complement1 [in Algebra.Parts2]
D
Def [in Algebra.Module_cat]Def [in Algebra.Complex_field]
Def [in Algebra.Sub_module]
Def [in Algebra.Sub_group]
Def [in Algebra.Group_kernel]
Def [in Algebra.Group_quotient]
Def [in Algebra.Endo_set]
Def [in Algebra.Group_of_group_hom]
Def [in Algebra.Operation_of_monoid]
Def [in Algebra.Fraction_field]
Def [in Algebra.Group_hom_factor]
Def [in Algebra.Sub_sgroup]
Def [in Algebra.Set_cat]
Def [in Algebra.Cartesian]
Def [in Algebra.Sub_monoid]
Def [in Algebra.Module_kernel]
Def.Hom [in Algebra.Module_cat]
Def.Module_def [in Algebra.Module_cat]
Def.Sub_module [in Algebra.Sub_module]
Def.Sub_group [in Algebra.Sub_group]
Def.Sub_sgroup [in Algebra.Sub_sgroup]
Def.Sub_monoid [in Algebra.Sub_monoid]
Diff [in Algebra.Diff]
F
Foncteurs [in Algebra.Categories2]Foncteurs.Def_1 [in Algebra.Categories2]
fparts_in_def [in Algebra.Fpart]
fparts2_def [in Algebra.Fpart2]
Free_monoid_def.Universal_prop [in Algebra.Free_monoid]
Free_monoid_def [in Algebra.Free_monoid]
Free_group_def.Universal_prop [in Algebra.Free_group]
Free_group_def [in Algebra.Free_group]
Free_abelian_monoid_def.Universal_prop [in Algebra.Free_abelian_monoid]
Free_abelian_monoid_def [in Algebra.Free_abelian_monoid]
Free_Module_def.Universal_prop [in Algebra.Free_module]
Free_Module_def [in Algebra.Free_module]
Free_abelian_group_def.Universal_prop [in Algebra.Free_abelian_group]
Free_abelian_group_def [in Algebra.Free_abelian_group]
G
Generated_monoid_def [in Algebra.Generated_monoid]Generated_group_def [in Algebra.Generated_group]
Generated_ideal [in Algebra.Ideal]
Generated_module_def [in Algebra.Generated_module]
Group [in Algebra.Group_util]
Group [in Algebra.Abelian_group_facts]
H
Hom [in Algebra.Group_util]Hom [in Algebra.Ring_cat]
Hom [in Algebra.Monoid_cat]
Hom [in Algebra.Sgroup_cat]
Hom [in Algebra.Module_util]
Hom [in Algebra.Monoid_util]
Hom [in Algebra.Ring_util]
Hom_module_def [in Algebra.Hom_module]
Hom_lemmas [in Algebra.Ring_facts]
I
ideals [in Algebra.Ideal]Images1 [in Algebra.Parts2]
Image_hom [in Algebra.Monoid_kernel]
Inclusion [in Algebra.Parts]
Injection [in Algebra.Sub_module]
Injection [in Algebra.Sub_group]
Injection [in Algebra.Sub_sgroup]
Injection [in Algebra.Sub_monoid]
Inter1 [in Algebra.Inter]
Int_power [in Algebra.Z_group]
Int_power [in Algebra.Group_power]
Inverse [in Algebra.Group_cat]
Inverse_image1.Inverse_image1_1 [in Algebra.Parts3]
Inverse_image1 [in Algebra.Parts3]
L
Lemmas [in Algebra.Algebra_facts]Lemmas [in Algebra.Group_facts]
Lemmas [in Algebra.Z_group_facts]
Lemmas [in Algebra.Integral_domain_facts]
Lemmas [in Algebra.Monoid_facts]
Lemmas [in Algebra.Ring_facts]
Lemmas [in Algebra.Group_power]
Lemmas [in Algebra.Module_facts]
Lemmas [in Algebra.Sgroup_facts]
Lemmas1 [in Algebra.Field_facts]
Lemmas1 [in Algebra.Cfield_facts]
Lemmas2 [in Algebra.Algebra_facts]
Lemmas2 [in Algebra.Group_facts]
M
Maps [in Algebra.Cartesian]Module [in Algebra.Module_util]
Module_on_group [in Algebra.Module_util]
Monoid [in Algebra.Abelian_group_facts]
Monoid [in Algebra.Monoid_util]
O
Objects [in Algebra.Integral_domain_cat]Objects [in Algebra.Ring_cat]
P
Part_set_greater [in Algebra.Parts]Part_set [in Algebra.Parts]
Part_type [in Algebra.Parts]
Projections [in Algebra.Cartesian]
R
Restrictions1 [in Algebra.Parts3]Ring [in Algebra.Ring_util]
Ring_algebra_as_ring [in Algebra.Algebra_facts]
Ring_as_module [in Algebra.Ideal]
S
Sets1 [in Algebra.Sets]Sets1.Maps1 [in Algebra.Sets]
Sets1.Maps1.Maps1_3 [in Algebra.Sets]
Sets1.Maps1.Maps1_2 [in Algebra.Sets]
Sets1.Maps1.Maps1_1 [in Algebra.Sets]
Sets1.Quotient1 [in Algebra.Sets]
Sets1.Relations [in Algebra.Sets]
Sgroup [in Algebra.Abelian_group_facts]
Single1 [in Algebra.Singleton]
Subcategory_def [in Algebra.Subcat]
Subtype [in Algebra.Parts]
T
tiroirs_def [in Algebra.Tiroirs]U
Union_of_part [in Algebra.Parts]Union1 [in Algebra.Union]
Unit [in Algebra.Monoid_cat]
Z
Zup1 [in Algebra.ZUP]Zup1 [in Algebra.Z_group]
Zup2 [in Algebra.Z_group]
Zup2.pos_def [in Algebra.Z_group]
Definition Index
A
ABELIAN_GROUP [in Algebra.Abelian_group_cat]ABELIAN_MONOID [in Algebra.Abelian_group_cat]
ABELIAN_SGROUP [in Algebra.Abelian_group_cat]
addfraction_fun [in Algebra.Fraction_field]
add_hom_module [in Algebra.Hom_module]
add_part [in Algebra.Fpart]
algebra_mult [in Algebra.Algebra]
app_rel [in Algebra.Sets]
asg [in Algebra.Group_util]
asg [in Algebra.Monoid_util]
associative [in Algebra.Sgroup_cat]
B
bijective [in Algebra.Sets]bij_group_quo_ker_coKer [in Algebra.Group_hom_factor]
BUILD_SUB_GROUP [in Algebra.Group_util]
BUILD_HOM_GROUP [in Algebra.Group_util]
BUILD_ABELIAN_GROUP [in Algebra.Group_util]
BUILD_GROUP [in Algebra.Group_util]
BUILD_MODULE_GROUP [in Algebra.Module_util]
BUILD_HOM_MODULE [in Algebra.Module_util]
BUILD_MODULE [in Algebra.Module_util]
BUILD_SUB_MONOID [in Algebra.Monoid_util]
BUILD_HOM_MONOID [in Algebra.Monoid_util]
BUILD_ABELIAN_MONOID [in Algebra.Monoid_util]
BUILD_MONOID [in Algebra.Monoid_util]
BUILD_HOM_RING [in Algebra.Ring_util]
BUILD_RING [in Algebra.Ring_util]
C
Cadd [in Algebra.Complex_field]cart [in Algebra.Cartesian]
cart_eq [in Algebra.Cartesian]
CC [in Algebra.Complex_field]
Ccring [in Algebra.Complex_field]
CdivR [in Algebra.Complex_field]
Ceq [in Algebra.Complex_field]
CFIELD [in Algebra.Cfield_cat]
Cinv [in Algebra.Complex_field]
Cinv_map [in Algebra.Complex_field]
Cmult [in Algebra.Complex_field]
coKer [in Algebra.Group_kernel]
coKer [in Algebra.Module_kernel]
commutative [in Algebra.Abelian_group_cat]
compl [in Algebra.Parts2]
comp_hom [in Algebra.Categories]
comp_map_map [in Algebra.Sets]
comp_map_fun [in Algebra.Sets]
Cone [in Algebra.Complex_field]
conjugate [in Algebra.Complex_field]
Copp [in Algebra.Complex_field]
couple [in Algebra.Cartesian]
Cring [in Algebra.Complex_field]
CRING [in Algebra.Ring_cat]
cring_monoid [in Algebra.Ring_cat]
Cset [in Algebra.Complex_field]
curry [in Algebra.Cartesian]
Czero [in Algebra.Complex_field]
C_field_on [in Algebra.Complex_field]
D
diff [in Algebra.Diff]disjoint [in Algebra.Fpart2]
dist_l [in Algebra.Ring_cat]
dist_r [in Algebra.Ring_cat]
E
empty [in Algebra.Parts]Endo_SET [in Algebra.Endo_set]
Endo_SET_sgroup [in Algebra.Endo_set]
endo_comp [in Algebra.Endo_set]
eqfraction [in Algebra.Fraction_field]
equivalence [in Algebra.Sets]
eq_part [in Algebra.Parts]
F
f [in Algebra.Group_util]f [in Algebra.Monoid_util]
FaG_var [in Algebra.Free_abelian_group]
FaG_lift [in Algebra.Free_abelian_group]
FaG_lift_fun [in Algebra.Free_abelian_group]
FaG_set [in Algebra.Free_abelian_group]
FaM_var [in Algebra.Free_abelian_monoid]
FaM_lift [in Algebra.Free_abelian_monoid]
FaM_lift_fun [in Algebra.Free_abelian_monoid]
FaM_set [in Algebra.Free_abelian_monoid]
FG_var [in Algebra.Free_group]
FG_lift [in Algebra.Free_group]
FG_lift_fun [in Algebra.Free_group]
FG_set [in Algebra.Free_group]
fhomsg [in Algebra.Group_util]
fhomsg [in Algebra.Monoid_util]
FIELD [in Algebra.Field_cat]
field_div [in Algebra.Field_facts]
field_inverse [in Algebra.Field_facts]
finite [in Algebra.Fmap]
FMd_var [in Algebra.Free_module]
FMd_lift [in Algebra.Free_module]
FMd_lift_fun [in Algebra.Free_module]
FMd_set [in Algebra.Free_module]
FM_var [in Algebra.Free_monoid]
FM_lift [in Algebra.Free_monoid]
FM_lift_fun [in Algebra.Free_monoid]
FM_set [in Algebra.Free_monoid]
fraction_cfield [in Algebra.Fraction_field]
fraction_set [in Algebra.Fraction_field]
fraction0 [in Algebra.Fraction_field]
fraction1 [in Algebra.Fraction_field]
fract_field_ring [in Algebra.Fraction_field]
fract_field_ring_aux [in Algebra.Fraction_field]
FreeAbelianGroup [in Algebra.Free_abelian_group]
FreeAbelianMonoid [in Algebra.Free_abelian_monoid]
FreeGroup [in Algebra.Free_group]
FreeModule [in Algebra.Free_module]
FreeMonoid [in Algebra.Free_monoid]
fsubcat_Hom_id [in Algebra.Categories]
fsubcat_Hom_comp [in Algebra.Categories]
fsubcat_Hom [in Algebra.Categories]
full [in Algebra.Parts]
full_subcat [in Algebra.Categories]
full_to_set [in Algebra.Parts]
fun_compatible [in Algebra.Sets]
fun2_compatible [in Algebra.Cartesian]
f2 [in Algebra.Group_util]
f2 [in Algebra.Monoid_util]
G
G [in Algebra.Group_util]G [in Algebra.Ring_util]
generated_monoid [in Algebra.Generated_monoid]
generated_group [in Algebra.Generated_group]
generated_ideal [in Algebra.Ideal]
generated_module_subgroup [in Algebra.Ideal]
generated_module [in Algebra.Generated_module]
GROUP [in Algebra.Group_cat]
group_of_subgroup [in Algebra.Sub_group]
group_quo_ker [in Algebra.Group_kernel]
group_quo_surj [in Algebra.Group_quotient]
group_quo [in Algebra.Group_quotient]
group_quo_set [in Algebra.Group_quotient]
group_quo_eqrel [in Algebra.Group_quotient]
group_quo_eq [in Algebra.Group_quotient]
group_hom [in Algebra.Group_of_group_hom]
group_hom_inv [in Algebra.Group_of_group_hom]
group_hom_unit [in Algebra.Group_of_group_hom]
group_hom_law [in Algebra.Group_of_group_hom]
group_inverse [in Algebra.Group_cat]
group_power [in Algebra.Z_group]
group_square [in Algebra.Z_group]
group_power [in Algebra.Group_power]
group_power_pos [in Algebra.Group_power]
group_square [in Algebra.Group_power]
H
Hom_module [in Algebra.Hom_module]Hom_comp_unit_r [in Algebra.Categories]
Hom_comp_unit_l [in Algebra.Categories]
Hom_comp_assoc [in Algebra.Categories]
I
Id [in Algebra.Sets]idomain_prop [in Algebra.Integral_domain_cat]
id_map_parts_equal [in Algebra.Parts]
image [in Algebra.Parts2]
image_map [in Algebra.Parts2]
image_monoid_hom [in Algebra.Monoid_kernel]
included [in Algebra.Parts]
injective [in Algebra.Sets]
inj_submodule [in Algebra.Sub_module]
inj_subgroup [in Algebra.Sub_group]
inj_part_included [in Algebra.Parts]
inj_part [in Algebra.Parts]
inj_coKer_group [in Algebra.Group_hom_factor]
inj_subsgroup [in Algebra.Sub_sgroup]
inj_submonoid [in Algebra.Sub_monoid]
INTEGRAL_DOMAIN [in Algebra.Integral_domain_cat]
inter [in Algebra.Inter]
inv [in Algebra.Group_util]
inverse_l [in Algebra.Group_cat]
inverse_r [in Algebra.Group_cat]
invfraction [in Algebra.Fraction_field]
invfraction_fun [in Algebra.Fraction_field]
invimage [in Algebra.Parts3]
in_part [in Algebra.Parts]
is_ideal [in Algebra.Ideal]
K
Ker [in Algebra.Group_kernel]Ker [in Algebra.Module_kernel]
kernel_part [in Algebra.Group_kernel]
L
law_of_composition [in Algebra.Sgroup_cat]Leibnitz_set [in Algebra.Sets]
M
m [in Algebra.Group_util]M [in Algebra.Monoid_util]
M [in Algebra.Ring_util]
MAP [in Algebra.Sets]
Map_eq [in Algebra.Sets]
map_couple [in Algebra.Cartesian]
map_proj2 [in Algebra.Cartesian]
map_proj1 [in Algebra.Cartesian]
minus_part [in Algebra.Fpart]
MODULE [in Algebra.Module_cat]
module_id [in Algebra.Module_cat]
module_hom_comp [in Algebra.Module_cat]
module_hom_prop [in Algebra.Module_cat]
module_mult [in Algebra.Module_cat]
module_of_submodule [in Algebra.Sub_module]
module_util_op2 [in Algebra.Module_util]
module_util_endo_el2 [in Algebra.Module_util]
module_util_G [in Algebra.Module_util]
module_util_op [in Algebra.Module_util]
module_util_endo_el [in Algebra.Module_util]
MONOID [in Algebra.Monoid_cat]
monoid_id [in Algebra.Monoid_cat]
monoid_hom_comp [in Algebra.Monoid_cat]
monoid_hom_prop [in Algebra.Monoid_cat]
monoid_of_submonoid [in Algebra.Sub_monoid]
multfraction_fun [in Algebra.Fraction_field]
mult_hom_module [in Algebra.Hom_module]
N
nat_to_group [in Algebra.Z_group]normal [in Algebra.Group_quotient]
O
operation [in Algebra.Operation_of_monoid]opfraction_fun [in Algebra.Fraction_field]
opp_hom_module [in Algebra.Hom_module]
op_lin_right [in Algebra.Module_cat]
op_lin_left [in Algebra.Module_cat]
P
part [in Algebra.Parts]partial_equivalence [in Algebra.Sets]
part_set [in Algebra.Parts]
pos_to_group [in Algebra.Z_group]
pos_abs [in Algebra.Z_group]
pred_compatible [in Algebra.Parts]
proj1 [in Algebra.Cartesian]
proj1_map [in Algebra.Cartesian]
proj2 [in Algebra.Cartesian]
proj2_map [in Algebra.Cartesian]
Q
Q [in Algebra.Qfield]quotient [in Algebra.Sets]
R
reflexive [in Algebra.Sets]relation [in Algebra.Sets]
rel_compatible [in Algebra.Sets]
restrict [in Algebra.Parts3]
RING [in Algebra.Ring_cat]
ring_algebra_ring [in Algebra.Algebra_facts]
ring_id [in Algebra.Ring_cat]
ring_hom_comp [in Algebra.Ring_cat]
ring_mult_hom_prop [in Algebra.Ring_cat]
ring_mult_hom_unit_prop [in Algebra.Ring_cat]
ring_unit [in Algebra.Ring_cat]
ring_mult [in Algebra.Ring_cat]
ring_module [in Algebra.Ideal]
S
SET [in Algebra.Set_cat]set_to_full [in Algebra.Parts]
set_of_subtype_image [in Algebra.Parts]
sg [in Algebra.Group_util]
sg [in Algebra.Monoid_util]
SGROUP [in Algebra.Sgroup_cat]
sgroup_of_subsgroup [in Algebra.Sub_sgroup]
sgroup_id [in Algebra.Sgroup_cat]
sgroup_hom_comp [in Algebra.Sgroup_cat]
sgroup_hom_prop [in Algebra.Sgroup_cat]
sgroup_law [in Algebra.Sgroup_cat]
sgroup_powers [in Algebra.Z_group]
single [in Algebra.Singleton]
subcat [in Algebra.Subcat]
subcat_Hom_comp [in Algebra.Subcat]
subcat_Hom [in Algebra.Subcat]
subgroup_group [in Algebra.Sub_group]
subgroup_inv [in Algebra.Sub_group]
submodule_module [in Algebra.Sub_module]
submodule_op [in Algebra.Sub_module]
submonoid_monoid [in Algebra.Sub_monoid]
subsgroup_sgroup [in Algebra.Sub_sgroup]
subsgroup_law [in Algebra.Sub_sgroup]
subtype_image_set [in Algebra.Parts]
subtype_image_equal [in Algebra.Parts]
surjective [in Algebra.Sets]
surj_part_image [in Algebra.Parts2]
surj_set_image [in Algebra.Parts2]
surj_set_quo [in Algebra.Sets]
surj_group_quo_ker [in Algebra.Group_hom_factor]
symmetric [in Algebra.Sets]
T
transitive [in Algebra.Sets]U
uncurry [in Algebra.Cartesian]union [in Algebra.Union]
union_part [in Algebra.Parts]
unit_l [in Algebra.Monoid_cat]
unit_r [in Algebra.Monoid_cat]
Z
zero_hom_module [in Algebra.Hom_module]Zr [in Algebra.Zring]
Zr_aux [in Algebra.Zring]
ZZ [in Algebra.Zring]
Zzero_dec [in Algebra.Zring]
Z_to_ring [in Algebra.ZUP]
Z_to_group [in Algebra.Z_group]
Z_to_group_fun [in Algebra.Z_group]
Z_to_group_nat [in Algebra.Z_group]
Z_to_group_nat_fun [in Algebra.Z_group]
Record Index
A
abelian_group [in Algebra.Abelian_group_cat]abelian_group_on [in Algebra.Abelian_group_cat]
abelian_monoid [in Algebra.Abelian_group_cat]
abelian_monoid_on [in Algebra.Abelian_group_cat]
abelian_sgroup [in Algebra.Abelian_group_cat]
abelian_sgroup_on [in Algebra.Abelian_group_cat]
algebra [in Algebra.Algebra]
algebra_on [in Algebra.Algebra]
C
cart_type [in Algebra.Cartesian]category [in Algebra.Categories]
cfield [in Algebra.Cfield_cat]
Cfunctor [in Algebra.Categories2]
cring [in Algebra.Ring_cat]
cring_on [in Algebra.Ring_cat]
Ctype [in Algebra.Complex_field]
F
field [in Algebra.Field_cat]field_on [in Algebra.Field_cat]
fraction [in Algebra.Fraction_field]
functor [in Algebra.Categories2]
G
group [in Algebra.Group_cat]group_on [in Algebra.Group_cat]
I
ideal [in Algebra.Ideal]idomain [in Algebra.Integral_domain_cat]
idomain_on [in Algebra.Integral_domain_cat]
M
Map [in Algebra.Sets]module [in Algebra.Module_cat]
module_hom [in Algebra.Module_cat]
module_on [in Algebra.Module_cat]
monoid [in Algebra.Monoid_cat]
monoid_hom [in Algebra.Monoid_cat]
monoid_on [in Algebra.Monoid_cat]
P
Predicate [in Algebra.Parts]R
Relation [in Algebra.Sets]ring [in Algebra.Ring_cat]
ring_algebra [in Algebra.Algebra]
ring_algebra_on [in Algebra.Algebra]
ring_hom [in Algebra.Ring_cat]
ring_on [in Algebra.Ring_cat]
S
Setoid [in Algebra.Sets]sgroup [in Algebra.Sgroup_cat]
sgroup_hom [in Algebra.Sgroup_cat]
sgroup_on [in Algebra.Sgroup_cat]
subgroup [in Algebra.Sub_group]
submodule [in Algebra.Sub_module]
submonoid [in Algebra.Sub_monoid]
subsgroup [in Algebra.Sub_sgroup]
subtype [in Algebra.Parts]
subtype_image [in Algebra.Parts]
| 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 | (1509 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 | (352 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 | (72 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 | (419 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 | (72 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 | (18 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 | (11 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 | (112 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 | (125 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 | (280 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 | (48 entries) |