groups_1 Theory

Summation and exponentiation functions are defined that draw indices from integer subranges and basic properties are proved about them.

Note that more general summation functions can be found in the list_2 and mset theories.

Summary of Definitions

Typed Definitions

monoid_p *1

group_p *1

grp_sig *1

grp_car *1

grp_eq *1

grp_le *1

grp_op *1 *6

grp_id *1 *2

grp_inv *1

imon *1

mon *1

iabmonoid *1

abmonoid *1

igrp *1

mk_igrp *5

grp *1

subgrp_p *1

norm_subset_p *1

norm_subgrp *1

eqv_mod_subset *1

iabgrp *1

quot_grp_car ?6

abgrp *1

monoid_hom_p *1

mon_hom_inj_p *1

monoid_hom *1

inj_mon_hom *1

dset_of_mon *1 *6 *2

omon *1

ocmon *1

oset_of_ocmon *1 *5

grp_leq *1

grp_lt *1

grp_blt *1

ocgrp *1

hgrp_car *1

hgrp_of_ocgrp *1 *8

itop *18

nat_op *1

int_op *7

mon_itop *2

mon_nat_op *1 *0 *7

comp_id_mon *13

bor_mon *19

band_mon *19

int_add_grp *9 *9

nat_add_mon *1 *5

mon_when *1

int_hgrp_el *1

int_hgrp_to_nat *1

Main Theorems

sq_stable__monoid_p *1

sq_stable__group_p *1

grp_op_l *2

grp_op_r *2

mk_imon *5

mon_ident *4

mon_assoc *3

mk_mon *4

assert_of_mon_eq *5

decidable__mon_eq *5

grp_eq_sym *3

abmonoid_comm *2

abmonoid_ac_1 *4

mk_abmonoid *5

grp_inverse *2

grp_op_cancel_l *11

grp_op_cancel_r *10

grp_inv_id *5

grp_inv_inv *6

grp_inv_assoc *8

grp_inv_thru_op *7

grp_eq_op_l *3

grp_eq_op_r *3

grp_eq_shift_right *3

grp_inv_diff *1

mk_grp *5

eqv_mod_subset_is_eqv *1

iabgrp_op_inv_assoc *4

sq_stable__monoid_hom_p *1

monoid_hom_id *3

monoid_hom_op *3

grp_hom_formation *4

grp_hom_inv *5

ident_mon_hom_shift *6

inverse_grp_sig_hom_shift *6

mon_hom_p_id *1

mon_hom_p_comp *4

ocmon_refl *1

ocmon_trans *1

ocmon_anti_sym *1

ocmon_connex *1

ocmon_cancel *1

ocmon_6 *1

sq_stable__grp_leq *1

grp_leq_iff_lt_or_eq *2

decidable__grp_lt *2

grp_lt_is_sp_of_leq_a *2

grp_lt_trans *2

grp_lt_irreflexivity *2

grp_lt_transitivity_2 *2

grp_lt_transitivity_1 *2

grp_leq_weakening_eq *2

grp_leq_weakening_lt *2

grp_leq_transitivity *2

omon_lt_mono_imp_leq_mono *7

grp_leq_antisymmetry *2

grp_leq_complement *2

grp_lt_complement *2

grp_lt_trichot *2

grp_op_preserves_le *3

grp_op_preserves_lt *9

grp_leq_op_l *4

grp_lt_op_l *4

grp_op_polarity *4

assert_of_grp_blt *2

ocgrp_inverse *1

grp_lt_shift_right *3

grp_leq_shift_right *3

inj_into_ocmon *22

itop_unroll_base *7

itop_unroll_hi *7

itop_unroll_unit *6

itop_unroll_lo *14

itop_shift *9

itop_split *14

nat_op_zero *3

nat_op_add *8

int_op_minus *12

mon_itop_unroll_base *1

mon_itop_unroll_hi *1

mon_itop_unroll_unit *1

mon_itop_unroll_lo *1

mon_itop_shift *1

mon_itop_split *1

mon_itop_split_el *4

mon_itop_op *8

mon_nat_op_zero *1

mon_nat_op_unroll *4

mon_nat_op_one *4

mon_nat_op_id *9

mon_nat_op_op *10

mon_nat_op_add *1

mon_nat_op_hom_swap *6

mon_nat_op_mul *36

nat_int_grp_sig_hom *2

nat_op_mon_hom_1 *2

nat_op_mon_hom_2 *2

nat_op_on_nat_add_mon *11

mon_when_false *3

mon_when_true *3

mon_when_of_id *6

mon_when_thru_op *4

mon_when_when *6

mon_when_swap *6

mon_when_is_hom *3

mon_when_hom_swap *5

zhgrp_to_nat_is_hom *6

zhgrp_op_mon_hom_1 *5