rings_1 Theory

There were several problems with this theory. Firstly, the type theory didn't support reasoning smoothly with ideals: ideals had to be defined as prop-valued predicates, with the result that reasoning about set operations on them was awkward.

Also, the type theory's constructivity forced the provision of `detaching functions' for ideals, and it was clumsy having to carry these around as well.

Summary of Definitions

Typed Definitions

rng_sig *1

rng_car *1

rng_eq *1

rng_le *1

rng_plus *1

rng_zero *1

rng_minus *1

rng_times *1

rng_one *1

rng_div *1

ring_p *1

rng *1

crng *1

mul_mon_of_rng *1 *4 *4 *6

add_grp_of_rng *1 *5 *9

rng_sum *1

rng_prod *1

nsgrp_of_ideal *1

ring_divs *1

ring_non_triv *1

integ_dom_p *1

field_p *1

integ_dom *1

field *

rprime *1

ideal_p *1

ideal *1

zero_ideal *

one_ideal *

princ_ideal *1

quot_ring_car *12

quot_ring *1

prime_ideal_p *1

max_ideal_p *1

rng_hom_p *1

rng_chom_p *1

ring_hom *1

ring_quot_hom *

int_ring *

int_pi_det_fun *1

choose *6

rng_nexp *1

rng_nat_op *1

rng_when *1

Main Theorems

assert_of_rng_eq *2

decidable__rng_eq *7

rng_minus_over_plus *1

rng_minus_minus *1

rng_minus_zero *1

rng_plus_inv *1

rng_plus_inv_assoc *1

rng_plus_zero *1

rng_plus_cancel_l *1

rng_plus_assoc *1

rng_times_assoc *1

rng_times_one *1

crng_times_comm *1

crng_times_ac_1 *1

rng_times_over_plus *3

rng_times_zero *11

rng_times_over_minus *12

rng_plus_comm *13

rng_plus_ac_1 *1

ring_triv *3

sq_stable__integ_dom_p *3

ideal_defines_eqv *1

det_ideal_ap_elim *9

det_ideal_defines_eqv *8

quot_ring_car_elim *7

quot_ring_car_elim_a *6

quot_ring_car_elim_b *1

all_rng_quot_elim *1

all_rng_quot_elim_a *2

sq_stable__prime_ideal *4

idom_alt_char *9

quot_by_prime_ideal *9

princ_ideal_mem_cond *9

ideal_of_prime *8

int_pi_detach *1

prime_ideals_in_int_ring *1

rng_nexp_zero *1

rng_nexp_unroll *2

rng_nat_op_one *1

rng_nat_op_add *1

rng_sum_unroll_base *2

rng_sum_unroll_hi *2

rng_sum_unroll_unit *2

rng_sum_unroll_lo *2

rng_sum_shift *1

rng_sum_split *1

rng_sum_plus *1

rng_times_sum_l *9

rng_times_sum_r *9

rng_times_nat_op *4

rng_times_nat_op_r *4

binomial *31

sum_of_geometric_prog *8

rng_times_when_l *4

rng_times_when_r *4

rng_when_of_zero *1

rng_when_thru_plus *1

rng_when_when *1

rng_when_swap *1