Structure ringTheory
signature ringTheory =
sig
type thm = Thm.thm
(* Definitions *)
val EuclideanRing_def : thm
val FiniteIntegralDomain_def : thm
val FiniteRing_def : thm
val IntegralDomain_def : thm
val PrincipalIdealRing_def : thm
val RingAuto_def : thm
val RingEndo_def : thm
val RingHomo_def : thm
val RingIso_def : thm
val Ring_def : thm
val ZN_def : thm
val ZP_def : thm
val Z_add_def : thm
val Z_def : thm
val Z_ideal_def : thm
val Z_mult_def : thm
val Z_multiple_def : thm
val char_def : thm
val compute_ordz_def : thm
val homo_ideal_def : thm
val homo_ring_def : thm
val ideal_congruence_def : thm
val ideal_coset_add_def : thm
val ideal_coset_mult_def : thm
val ideal_def : thm
val ideal_gen_def : thm
val ideal_maximal_def : thm
val ideal_sum_def : thm
val irreducible_def : thm
val kernel_ideal_def : thm
val monoid_of_ring_nonzero_mult_def : thm
val principal_ideal_def : thm
val quotient_ring_add_def : thm
val quotient_ring_def : thm
val quotient_ring_mult_def : thm
val recordtype_ring_seldef_carrier_def : thm
val recordtype_ring_seldef_carrier_fupd_def : thm
val recordtype_ring_seldef_prod_def : thm
val recordtype_ring_seldef_prod_fupd_def : thm
val recordtype_ring_seldef_sum_def : thm
val recordtype_ring_seldef_sum_fupd_def : thm
val ring_TY_DEF : thm
val ring_associates_def : thm
val ring_case_def : thm
val ring_divides_def : thm
val ring_fun_def : thm
val ring_gcd_def : thm
val ring_homo_image_def : thm
val ring_inj_image_def : thm
val ring_list_def : thm
val ring_nonzero_def : thm
val ring_ordering_def : thm
val ring_prime_def : thm
val ring_size_def : thm
val ring_sub_def : thm
val ring_sum_def : thm
val subring_def : thm
val symdiff_set_inter_def : thm
val trivial_integal_domain_def : thm
val trivial_ring_def : thm
val unit_eq_def : thm
(* Theorems *)
val EXISTS_ring : thm
val FORALL_ring : thm
val LIST_REL_ring_associates_product : thm
val WHILE_RULE_PRE_POST : thm
val ZN_1_exp : thm
val ZN_card : thm
val ZN_char : thm
val ZN_coprime_euler_element : thm
val ZN_coprime_exp_mod : thm
val ZN_coprime_invertible : thm
val ZN_coprime_order : thm
val ZN_coprime_order_alt : thm
val ZN_coprime_order_divides_phi : thm
val ZN_coprime_order_divides_totient : thm
val ZN_coprime_order_gt_1 : thm
val ZN_coprime_order_lt : thm
val ZN_eval : thm
val ZN_exp : thm
val ZN_finite : thm
val ZN_finite_ring : thm
val ZN_ids : thm
val ZN_ids_alt : thm
val ZN_invertibles : thm
val ZN_invertibles_finite_group : thm
val ZN_invertibles_group : thm
val ZN_invertibles_order : thm
val ZN_mult_inv_coprime : thm
val ZN_mult_inv_coprime_iff : thm
val ZN_not_coprime : thm
val ZN_num : thm
val ZN_num_0 : thm
val ZN_num_1 : thm
val ZN_num_mod : thm
val ZN_order_0 : thm
val ZN_order_1 : thm
val ZN_order_divides_exp : thm
val ZN_order_divides_phi : thm
val ZN_order_divides_tops_index : thm
val ZN_order_divisibility : thm
val ZN_order_eq_0 : thm
val ZN_order_eq_0_iff : thm
val ZN_order_eq_0_test : thm
val ZN_order_eq_1 : thm
val ZN_order_eq_1_alt : thm
val ZN_order_eq_1_by_prime_factors : thm
val ZN_order_gt_1_property : thm
val ZN_order_le : thm
val ZN_order_le_tops_index : thm
val ZN_order_lt : thm
val ZN_order_minimal : thm
val ZN_order_mod : thm
val ZN_order_mod_1 : thm
val ZN_order_nonzero : thm
val ZN_order_nonzero_iff : thm
val ZN_order_property : thm
val ZN_order_property_alt : thm
val ZN_order_test_1 : thm
val ZN_order_test_2 : thm
val ZN_order_test_3 : thm
val ZN_order_test_4 : thm
val ZN_order_test_propery : thm
val ZN_order_upper : thm
val ZN_order_with_coprime_1 : thm
val ZN_order_with_coprime_2 : thm
val ZN_property : thm
val ZN_ring : thm
val ZN_to_ZN_element : thm
val ZN_to_ZN_prod_monoid_homo : thm
val ZN_to_ZN_ring_homo : thm
val ZN_to_ZN_sum_group_homo : thm
val ZP_finite : thm
val ZP_finite_integral_domain : thm
val ZP_integral_domain : thm
val Z_add_abelian_group : thm
val Z_add_group : thm
val Z_add_inv : thm
val Z_euclid_ring : thm
val Z_ideal_map_bij : thm
val Z_ideal_map_element : thm
val Z_ideal_map_group_homo : thm
val Z_ideal_map_monoid_homo : thm
val Z_ideal_sum_group : thm
val Z_ideal_sum_normal : thm
val Z_ideal_sum_subgroup : thm
val Z_ideal_thm : thm
val Z_mult_abelian_monoid : thm
val Z_mult_monoid : thm
val Z_multiple_less_neg_eq : thm
val Z_principal_ideal_ring : thm
val Z_quotient_iso_ZN : thm
val Z_ring : thm
val Z_sum_cogen : thm
val Z_sum_coset_eq : thm
val char_eq_0 : thm
val char_minimal : thm
val char_property : thm
val compute_ordz_0 : thm
val compute_ordz_1 : thm
val compute_ordz_eqn : thm
val compute_ordz_hoare : thm
val datatype_ring : thm
val euclid_ring_map : thm
val euclid_ring_principal_ideal_ring : thm
val euclid_ring_property : thm
val euclid_ring_ring : thm
val finite_integral_domain_nonzero_group : thm
val finite_integral_domain_nonzero_invertible : thm
val finite_integral_domain_nonzero_invertible_alt : thm
val finite_integral_domain_period_exists : thm
val finite_ring_add_finite_abelian_group : thm
val finite_ring_add_finite_group : thm
val finite_ring_card_eq_1 : thm
val finite_ring_card_pos : thm
val finite_ring_card_prime : thm
val finite_ring_char : thm
val finite_ring_char_alt : thm
val finite_ring_char_divides : thm
val finite_ring_char_pos : thm
val finite_ring_is_ring : thm
val finite_ring_mult_finite_abelian_monoid : thm
val finite_ring_mult_finite_monoid : thm
val homo_ring_by_inj : thm
val homo_ring_property : thm
val homo_ring_ring : thm
val homo_ring_subring : thm
val ideal_antisym : thm
val ideal_carrier_sing : thm
val ideal_carriers : thm
val ideal_cogen_property : thm
val ideal_congruence_elements : thm
val ideal_congruence_equiv : thm
val ideal_congruence_iff_inCoset : thm
val ideal_congruence_mult : thm
val ideal_congruence_refl : thm
val ideal_congruence_sym : thm
val ideal_congruence_trans : thm
val ideal_coset_add : thm
val ideal_coset_element : thm
val ideal_coset_eq : thm
val ideal_coset_eq_carrier : thm
val ideal_coset_eq_congruence : thm
val ideal_coset_has_gen_diff : thm
val ideal_coset_mult : thm
val ideal_coset_neg : thm
val ideal_coset_of_element : thm
val ideal_coset_property : thm
val ideal_coset_zero : thm
val ideal_element : thm
val ideal_element_property : thm
val ideal_eq_ideal : thm
val ideal_gen_exists : thm
val ideal_gen_minimal : thm
val ideal_has_diff : thm
val ideal_has_multiple : thm
val ideal_has_neg : thm
val ideal_has_one : thm
val ideal_has_principal_ideal : thm
val ideal_has_product : thm
val ideal_has_subgroup : thm
val ideal_has_sum : thm
val ideal_has_zero : thm
val ideal_in_quotient_ring : thm
val ideal_ops : thm
val ideal_product_property : thm
val ideal_property : thm
val ideal_refl : thm
val ideal_sub_ideal : thm
val ideal_sub_itself : thm
val ideal_subgroup_ideal_sum : thm
val ideal_sum_comm : thm
val ideal_sum_element : thm
val ideal_sum_group : thm
val ideal_sum_has_ideal : thm
val ideal_sum_has_ideal_comm : thm
val ideal_sum_ideal : thm
val ideal_sum_sub_ideal : thm
val ideal_sum_subgroup : thm
val ideal_with_one : thm
val ideal_with_unit : thm
val ideal_zero : thm
val integral_domain_char : thm
val integral_domain_divides_prime : thm
val integral_domain_exp_eq : thm
val integral_domain_exp_eq_zero : thm
val integral_domain_exp_nonzero : thm
val integral_domain_is_ring : thm
val integral_domain_mult_eq_zero : thm
val integral_domain_mult_lcancel : thm
val integral_domain_mult_nonzero : thm
val integral_domain_mult_rcancel : thm
val integral_domain_nonzero_monoid : thm
val integral_domain_nonzero_mult_carrier : thm
val integral_domain_nonzero_mult_is_monoid : thm
val integral_domain_nonzero_mult_property : thm
val integral_domain_nonzero_order : thm
val integral_domain_one_ne_zero : thm
val integral_domain_one_nonzero : thm
val integral_domain_order_eq_0 : thm
val integral_domain_order_nonzero : thm
val integral_domain_order_zero : thm
val integral_domain_prime_factors_unique : thm
val integral_domain_ring_iso : thm
val integral_domain_zero_not_unit : thm
val integral_domain_zero_product : thm
val irreducible_associates : thm
val irreducible_element : thm
val irreducible_factors : thm
val kernel_ideal_element : thm
val kernel_ideal_gen_add_map : thm
val kernel_ideal_gen_id_map : thm
val kernel_ideal_gen_mult_map : thm
val kernel_ideal_quotient_bij : thm
val kernel_ideal_quotient_element_eq : thm
val kernel_ideal_quotient_homo : thm
val kernel_ideal_quotient_inj : thm
val kernel_ideal_quotient_iso : thm
val kernel_ideal_quotient_surj : thm
val kernel_ideal_sum_eqn : thm
val ordz_eval : thm
val prime_is_irreducible : thm
val principal_ideal_element : thm
val principal_ideal_element_divides : thm
val principal_ideal_eq_principal_ideal : thm
val principal_ideal_equal_principal_ideal : thm
val principal_ideal_group : thm
val principal_ideal_has_element : thm
val principal_ideal_has_principal_ideal : thm
val principal_ideal_ideal : thm
val principal_ideal_property : thm
val principal_ideal_ring_atom_is_prime : thm
val principal_ideal_ring_ideal_maximal : thm
val principal_ideal_ring_irreducible_is_prime : thm
val principal_ideal_sub_implies_divides : thm
val principal_ideal_subgroup : thm
val principal_ideal_subgroup_normal : thm
val principal_ideal_sum_eq_ideal : thm
val principal_ideal_sum_equal_ideal : thm
val quotient_ring_add_abelian_group : thm
val quotient_ring_add_assoc : thm
val quotient_ring_add_comm : thm
val quotient_ring_add_element : thm
val quotient_ring_add_group : thm
val quotient_ring_add_id : thm
val quotient_ring_add_inv : thm
val quotient_ring_by_principal_ideal : thm
val quotient_ring_element : thm
val quotient_ring_has_ideal : thm
val quotient_ring_homo : thm
val quotient_ring_homo_kernel : thm
val quotient_ring_homo_kernel_ideal : thm
val quotient_ring_homo_surj : thm
val quotient_ring_mult_abelian_monoid : thm
val quotient_ring_mult_assoc : thm
val quotient_ring_mult_comm : thm
val quotient_ring_mult_element : thm
val quotient_ring_mult_id : thm
val quotient_ring_mult_ladd : thm
val quotient_ring_mult_monoid : thm
val quotient_ring_property : thm
val quotient_ring_ring : thm
val quotient_ring_ring_sing : thm
val ring_11 : thm
val ring_Axiom : thm
val ring_accessors : thm
val ring_accfupds : thm
val ring_add_abelian_group : thm
val ring_add_assoc : thm
val ring_add_assoc_comm : thm
val ring_add_char_2 : thm
val ring_add_comm : thm
val ring_add_element : thm
val ring_add_eq_zero : thm
val ring_add_exp_eqn : thm
val ring_add_group : thm
val ring_add_group_rwt : thm
val ring_add_lcancel : thm
val ring_add_lneg : thm
val ring_add_lneg_assoc : thm
val ring_add_lzero : thm
val ring_add_pair_sub : thm
val ring_add_rcancel : thm
val ring_add_rneg : thm
val ring_add_rneg_assoc : thm
val ring_add_rzero : thm
val ring_add_sub : thm
val ring_add_sub_assoc : thm
val ring_add_sub_comm : thm
val ring_add_sub_identity : thm
val ring_add_zero_zero : thm
val ring_associates_divides : thm
val ring_associates_mult : thm
val ring_associates_refl : thm
val ring_associates_sym : thm
val ring_associates_trans : thm
val ring_auto_I : thm
val ring_auto_bij : thm
val ring_auto_cong : thm
val ring_auto_element : thm
val ring_auto_ids : thm
val ring_auto_linv_auto : thm
val ring_auto_one : thm
val ring_auto_zero : thm
val ring_binomial_2 : thm
val ring_binomial_3 : thm
val ring_binomial_4 : thm
val ring_binomial_genlist_index_shift : thm
val ring_binomial_index_shift : thm
val ring_binomial_term_merge_x : thm
val ring_binomial_term_merge_y : thm
val ring_binomial_thm : thm
val ring_carrier_nonempty : thm
val ring_carriers : thm
val ring_case_cong : thm
val ring_case_eq : thm
val ring_char_0 : thm
val ring_char_1 : thm
val ring_char_2_double : thm
val ring_char_2_neg_one : thm
val ring_char_2_property : thm
val ring_char_alt : thm
val ring_char_divides : thm
val ring_char_eq_1 : thm
val ring_char_prime : thm
val ring_char_prime_endo : thm
val ring_component_equality : thm
val ring_divides_associates : thm
val ring_divides_by_one : thm
val ring_divides_by_unit : thm
val ring_divides_iso : thm
val ring_divides_le : thm
val ring_divides_refl : thm
val ring_divides_trans : thm
val ring_divides_zero : thm
val ring_eq_unit_eq : thm
val ring_exp_0 : thm
val ring_exp_1 : thm
val ring_exp_SUC : thm
val ring_exp_add : thm
val ring_exp_add_assoc : thm
val ring_exp_comm : thm
val ring_exp_element : thm
val ring_exp_mod_order : thm
val ring_exp_mult : thm
val ring_exp_mult_comm : thm
val ring_exp_neg : thm
val ring_exp_small : thm
val ring_exp_suc : thm
val ring_factor_multiple : thm
val ring_fermat_all : thm
val ring_fermat_thm : thm
val ring_first_isomorphism_thm : thm
val ring_fn_updates : thm
val ring_freshman_all : thm
val ring_freshman_all_sub : thm
val ring_freshman_thm : thm
val ring_freshman_thm_sub : thm
val ring_fun_add : thm
val ring_fun_from_ring_fun : thm
val ring_fun_from_ring_fun_exp : thm
val ring_fun_genlist : thm
val ring_fun_map : thm
val ring_fupdcanon : thm
val ring_fupdcanon_comp : thm
val ring_fupdfupds : thm
val ring_fupdfupds_comp : thm
val ring_gcd_divides : thm
val ring_gcd_element : thm
val ring_gcd_is_gcd : thm
val ring_gcd_linear : thm
val ring_gcd_property : thm
val ring_gcd_sym : thm
val ring_gcd_zero : thm
val ring_homo_I_refl : thm
val ring_homo_add : thm
val ring_homo_char_divides : thm
val ring_homo_compose : thm
val ring_homo_cong : thm
val ring_homo_element : thm
val ring_homo_eq_zero : thm
val ring_homo_exp : thm
val ring_homo_ideal_group : thm
val ring_homo_ideal_ideal : thm
val ring_homo_ideal_subgroup : thm
val ring_homo_ids : thm
val ring_homo_image_bij : thm
val ring_homo_image_carrier : thm
val ring_homo_image_homo : thm
val ring_homo_image_is_subring : thm
val ring_homo_image_iso : thm
val ring_homo_image_ring : thm
val ring_homo_image_subring : thm
val ring_homo_image_subring_subring : thm
val ring_homo_image_surj_property : thm
val ring_homo_inv : thm
val ring_homo_kernel_ideal : thm
val ring_homo_linv_homo : thm
val ring_homo_mult : thm
val ring_homo_neg : thm
val ring_homo_num : thm
val ring_homo_num_nonzero : thm
val ring_homo_one : thm
val ring_homo_one_eq_zero : thm
val ring_homo_property : thm
val ring_homo_ring_homo_subring : thm
val ring_homo_sub : thm
val ring_homo_subring_homo : thm
val ring_homo_sum_num_property : thm
val ring_homo_sym : thm
val ring_homo_sym_any : thm
val ring_homo_trans : thm
val ring_homo_unit : thm
val ring_homo_unit_inv : thm
val ring_homo_unit_inv_element : thm
val ring_homo_unit_inv_nonzero : thm
val ring_homo_unit_nonzero : thm
val ring_homo_zero : thm
val ring_induction : thm
val ring_inj_image_alt : thm
val ring_inj_image_carrier : thm
val ring_inj_image_prod_abelian_monoid : thm
val ring_inj_image_prod_monoid : thm
val ring_inj_image_prod_monoid_homo : thm
val ring_inj_image_ring : thm
val ring_inj_image_ring_homo : thm
val ring_inj_image_sum_abelian_group : thm
val ring_inj_image_sum_group : thm
val ring_inj_image_sum_group_homo : thm
val ring_inj_image_sum_monoid : thm
val ring_inv_one : thm
val ring_irreducible_gcd : thm
val ring_iso_I_refl : thm
val ring_iso_add : thm
val ring_iso_bij : thm
val ring_iso_card_eq : thm
val ring_iso_char_eq : thm
val ring_iso_compose : thm
val ring_iso_cong : thm
val ring_iso_element : thm
val ring_iso_element_unique : thm
val ring_iso_eq_one : thm
val ring_iso_eq_zero : thm
val ring_iso_exp : thm
val ring_iso_ids : thm
val ring_iso_inv : thm
val ring_iso_inverse : thm
val ring_iso_inverse_element : thm
val ring_iso_linv_iso : thm
val ring_iso_mult : thm
val ring_iso_neg : thm
val ring_iso_nonzero : thm
val ring_iso_num : thm
val ring_iso_one : thm
val ring_iso_property : thm
val ring_iso_ring_homo_subring : thm
val ring_iso_sub : thm
val ring_iso_subring_iso : thm
val ring_iso_sym : thm
val ring_iso_sym_any : thm
val ring_iso_trans : thm
val ring_iso_unit : thm
val ring_iso_zero : thm
val ring_list_SNOC : thm
val ring_list_cons : thm
val ring_list_from_genlist : thm
val ring_list_from_genlist_ring_fun : thm
val ring_list_front_last : thm
val ring_list_gen_from_ring_fun : thm
val ring_list_nil : thm
val ring_literal_11 : thm
val ring_literal_nchotomy : thm
val ring_mult_abelian_monoid : thm
val ring_mult_add : thm
val ring_mult_add_neg : thm
val ring_mult_add_neg_assoc : thm
val ring_mult_add_neg_mult : thm
val ring_mult_add_neg_mult_assoc : thm
val ring_mult_assoc : thm
val ring_mult_assoc_comm : thm
val ring_mult_comm : thm
val ring_mult_divides : thm
val ring_mult_element : thm
val ring_mult_exp : thm
val ring_mult_ladd : thm
val ring_mult_lneg : thm
val ring_mult_lone : thm
val ring_mult_lsub : thm
val ring_mult_lzero : thm
val ring_mult_monoid : thm
val ring_mult_monoid_rwt : thm
val ring_mult_neg_neg : thm
val ring_mult_one_one : thm
val ring_mult_pair_diff : thm
val ring_mult_pair_sub : thm
val ring_mult_radd : thm
val ring_mult_rneg : thm
val ring_mult_rone : thm
val ring_mult_rsub : thm
val ring_mult_rzero : thm
val ring_mult_zero_zero : thm
val ring_nchotomy : thm
val ring_neg_add : thm
val ring_neg_add_comm : thm
val ring_neg_add_neg : thm
val ring_neg_add_neg_assoc : thm
val ring_neg_add_neg_mult : thm
val ring_neg_add_neg_mult_assoc : thm
val ring_neg_char_2 : thm
val ring_neg_element : thm
val ring_neg_eq : thm
val ring_neg_eq_swap : thm
val ring_neg_eq_zero : thm
val ring_neg_exp : thm
val ring_neg_mult : thm
val ring_neg_mult_add_neg_mult : thm
val ring_neg_mult_add_neg_mult_assoc : thm
val ring_neg_neg : thm
val ring_neg_nonzero : thm
val ring_neg_one_eq_one : thm
val ring_neg_square : thm
val ring_neg_sub : thm
val ring_neg_zero : thm
val ring_nonzero_element : thm
val ring_nonzero_eq : thm
val ring_nonzero_mult_carrier : thm
val ring_num_0 : thm
val ring_num_1 : thm
val ring_num_2 : thm
val ring_num_SUC : thm
val ring_num_add : thm
val ring_num_add_assoc : thm
val ring_num_add_mult : thm
val ring_num_add_mult_assoc : thm
val ring_num_all_zero : thm
val ring_num_char_coprime_nonzero : thm
val ring_num_element : thm
val ring_num_eq : thm
val ring_num_exp : thm
val ring_num_mod : thm
val ring_num_mult : thm
val ring_num_mult_assoc : thm
val ring_num_mult_element : thm
val ring_num_mult_exp : thm
val ring_num_mult_neg : thm
val ring_num_mult_radd : thm
val ring_num_mult_small : thm
val ring_num_mult_suc : thm
val ring_num_negative : thm
val ring_num_one : thm
val ring_num_sub : thm
val ring_num_suc : thm
val ring_one_element : thm
val ring_one_eq_zero : thm
val ring_one_exp : thm
val ring_one_unique : thm
val ring_prime_divides_product : thm
val ring_prime_iso : thm
val ring_product_factors_divide : thm
val ring_single_add_mult : thm
val ring_single_add_mult_assoc : thm
val ring_single_add_neg_mult : thm
val ring_single_add_neg_mult_assoc : thm
val ring_single_add_single : thm
val ring_single_add_single_assoc : thm
val ring_single_mult_exp : thm
val ring_single_mult_exp_assoc : thm
val ring_single_mult_single : thm
val ring_single_mult_single_assoc : thm
val ring_sub_add : thm
val ring_sub_element : thm
val ring_sub_eq : thm
val ring_sub_eq_add : thm
val ring_sub_eq_zero : thm
val ring_sub_lcancel : thm
val ring_sub_pair_reduce : thm
val ring_sub_rcancel : thm
val ring_sub_zero : thm
val ring_sum_SNOC : thm
val ring_sum_append : thm
val ring_sum_cons : thm
val ring_sum_decompose_first : thm
val ring_sum_decompose_first_last : thm
val ring_sum_decompose_last : thm
val ring_sum_element : thm
val ring_sum_freshman_all : thm
val ring_sum_freshman_thm : thm
val ring_sum_fun_zero : thm
val ring_sum_genlist_add : thm
val ring_sum_genlist_append : thm
val ring_sum_genlist_const : thm
val ring_sum_genlist_sum : thm
val ring_sum_mult : thm
val ring_sum_mult_ladd : thm
val ring_sum_nil : thm
val ring_sum_sing : thm
val ring_sum_zero : thm
val ring_unit_element : thm
val ring_unit_has_inv : thm
val ring_unit_inv_element : thm
val ring_unit_inv_inv : thm
val ring_unit_inv_nonzero : thm
val ring_unit_linv : thm
val ring_unit_linv_inv : thm
val ring_unit_linv_unique : thm
val ring_unit_mult_eq_unit : thm
val ring_unit_mult_unit : thm
val ring_unit_mult_zero : thm
val ring_unit_neg : thm
val ring_unit_nonzero : thm
val ring_unit_one : thm
val ring_unit_property : thm
val ring_unit_rinv : thm
val ring_unit_rinv_inv : thm
val ring_unit_rinv_unique : thm
val ring_unit_zero : thm
val ring_units_abelain_group : thm
val ring_units_element : thm
val ring_units_group : thm
val ring_units_has_one : thm
val ring_units_has_zero : thm
val ring_units_property : thm
val ring_updates_eq_literal : thm
val ring_zero_divides : thm
val ring_zero_element : thm
val ring_zero_exp : thm
val ring_zero_fix : thm
val ring_zero_sub : thm
val ring_zero_unique : thm
val subring_I_antisym : thm
val subring_add : thm
val subring_by_subgroup_submonoid : thm
val subring_carrier_antisym : thm
val subring_carrier_finite : thm
val subring_carrier_subset : thm
val subring_char : thm
val subring_char_divides : thm
val subring_element : thm
val subring_element_alt : thm
val subring_exp : thm
val subring_finite_ring : thm
val subring_homo_homo : thm
val subring_ids : thm
val subring_mult : thm
val subring_neg : thm
val subring_num : thm
val subring_one : thm
val subring_prod_submonoid : thm
val subring_property : thm
val subring_refl : thm
val subring_ring_iso_compose : thm
val subring_ring_iso_ring_homo_subring : thm
val subring_sub : thm
val subring_sum_subgroup : thm
val subring_trans : thm
val subring_unit : thm
val subring_unit_inv : thm
val subring_unit_inv_element : thm
val subring_unit_inv_nonzero : thm
val subring_unit_nonzero : thm
val subring_zero : thm
val symdiff_eval : thm
val symdiff_set_inter_char : thm
val symdiff_set_inter_ring : thm
val symdiff_univ_univ_eq_empty : thm
val trivial_char : thm
val trivial_integral_domain : thm
val trivial_ring : thm
val trivial_ring_thm : thm
val unit_eq_refl : thm
val unit_eq_sym : thm
val unit_eq_trans : thm
val zero_ideal_ideal : thm
val zero_ideal_sing : thm
(*
[Omega] Parent theory of "ring"
[container] Parent theory of "ring"
[group] Parent theory of "ring"
[EuclideanRing_def] Definition
⊢ ∀r f.
EuclideanRing r f ⇔
Ring r ∧ (∀x. f x = 0 ⇔ x = #0) ∧
∀x y.
x ∈ R ∧ y ∈ R ∧ y ≠ #0 ⇒
∃q t. q ∈ R ∧ t ∈ R ∧ x = q * y + t ∧ f t < f y
[FiniteIntegralDomain_def] Definition
⊢ ∀r. FiniteIntegralDomain r ⇔ IntegralDomain r ∧ FINITE R
[FiniteRing_def] Definition
⊢ ∀r. FiniteRing r ⇔ Ring r ∧ FINITE R
[IntegralDomain_def] Definition
⊢ ∀r. IntegralDomain r ⇔
Ring r ∧ #1 ≠ #0 ∧
∀x y. x ∈ R ∧ y ∈ R ⇒ (x * y = #0 ⇔ x = #0 ∨ y = #0)
[PrincipalIdealRing_def] Definition
⊢ ∀r. PrincipalIdealRing r ⇔
Ring r ∧ ∀i. i << r ⇒ ∃p. p ∈ R ∧ <p> = i
[RingAuto_def] Definition
⊢ ∀f r. RingAuto f r ⇔ RingIso f r r
[RingEndo_def] Definition
⊢ ∀f r. RingEndo f r ⇔ RingHomo f r r
[RingHomo_def] Definition
⊢ ∀f r s.
RingHomo f r s ⇔
(∀x. x ∈ R ⇒ f x ∈ s.carrier) ∧ GroupHomo f r.sum s.sum ∧
MonoidHomo f r.prod s.prod
[RingIso_def] Definition
⊢ ∀f r s. RingIso f r s ⇔ RingHomo f r s ∧ BIJ f R s.carrier
[Ring_def] Definition
⊢ ∀r. Ring r ⇔
AbelianGroup r.sum ∧ AbelianMonoid r.prod ∧ r.sum.carrier = R ∧
r.prod.carrier = R ∧
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * (y + z) = x * y + x * z
[ZN_def] Definition
⊢ ∀n. ZN n =
<|carrier := count n; sum := add_mod n; prod := times_mod n|>
[ZP_def] Definition
⊢ ∀p. ZP p =
<|carrier := count p; sum := add_mod p; prod := times_mod p|>
[Z_add_def] Definition
⊢ Z_add = <|carrier := 𝕌(:int); op := (λx y. x + y); id := 0|>
[Z_def] Definition
⊢ Z = <|carrier := 𝕌(:int); sum := Z_add; prod := Z_mult|>
[Z_ideal_def] Definition
⊢ ∀n. Z* n =
<|carrier := Z_multiple n;
sum :=
<|carrier := Z_multiple n; op := Z.sum.op; id := Z.sum.id|>;
prod :=
<|carrier := Z_multiple n; op := Z.prod.op;
id := Z.prod.id|> |>
[Z_mult_def] Definition
⊢ Z_mult = <|carrier := 𝕌(:int); op := (λx y. x * y); id := 1|>
[Z_multiple_def] Definition
⊢ ∀n. Z_multiple n = {&n * z | z ∈ 𝕌(:int)}
[char_def] Definition
⊢ ∀r. char r = order r.sum #1
[compute_ordz_def] Definition
⊢ ∀m n.
compute_ordz m n =
if m = 0 then ordz 0 n
else if m = 1 then 1
else if coprime m n then WHILE (λi. n ** i MOD m ≠ 1) SUC 1
else 0
[homo_ideal_def] Definition
⊢ ∀f r s i.
homo_ideal f r s i =
<|carrier := IMAGE f I;
sum := <|carrier := IMAGE f I; op := s.sum.op; id := f #0|>;
prod := <|carrier := IMAGE f I; op := s.prod.op; id := f #1|> |>
[homo_ring_def] Definition
⊢ ∀r f.
homo_ring r f =
<|carrier := IMAGE f R; sum := homo_group r.sum f;
prod := homo_group r.prod f|>
[ideal_congruence_def] Definition
⊢ ∀r i x y. x === y ⇔ x − y ∈ I
[ideal_coset_add_def] Definition
⊢ ∀r i x y. x + y = (gen x + gen y) ∘ I
[ideal_coset_mult_def] Definition
⊢ ∀r i x y. x * y = (gen x * gen y) ∘ I
[ideal_def] Definition
⊢ ∀i r.
i << r ⇔
i.sum ≤ r.sum ∧ i.sum.carrier = I ∧ i.prod.carrier = I ∧
i.prod.op = $* ∧ i.prod.id = #1 ∧
∀x y. x ∈ I ∧ y ∈ R ⇒ x * y ∈ I ∧ y * x ∈ I
[ideal_gen_def] Definition
⊢ ∀r i f.
Ring r ∧ i << r ∧ i ≠ <#0> ∧ (∀x. f x = 0 ⇔ x = #0) ⇒
ideal_gen r i f ∈ I ∧ ideal_gen r i f ≠ #0 ∧
∀z. z ∈ I ∧ z ≠ #0 ⇒ f (ideal_gen r i f) ≤ f z
[ideal_maximal_def] Definition
⊢ ∀r i. maxi i ⇔ i << r ∧ ∀j. i << j ∧ j << r ⇒ i = j ∨ j = r
[ideal_sum_def] Definition
⊢ ∀r i j.
i + j =
<|carrier := {x + y | x ∈ I ∧ y ∈ J};
sum :=
<|carrier := {x + y | x ∈ I ∧ y ∈ J}; op := $+; id := #0|>;
prod :=
<|carrier := {x + y | x ∈ I ∧ y ∈ J}; op := $*; id := #1|> |>
[irreducible_def] Definition
⊢ ∀r z.
atom z ⇔
z ∈ R+ ∧ z ∉ R* ∧
∀x y. x ∈ R ∧ y ∈ R ∧ z = x * y ⇒ unit x ∨ unit y
[kernel_ideal_def] Definition
⊢ ∀f r s.
kernel_ideal f r s =
<|carrier := kernel f r.sum s.sum;
sum := <|carrier := kernel f r.sum s.sum; op := $+; id := #0|>;
prod := <|carrier := kernel f r.sum s.sum; op := $*; id := #1|> |>
[monoid_of_ring_nonzero_mult_def] Definition
⊢ ∀r. monoid_of_ring_nonzero_mult r =
<|carrier := R+; op := $*; id := #1|>
[principal_ideal_def] Definition
⊢ ∀r p.
<p> =
<|carrier := p * R;
sum := <|carrier := p * R; op := $+; id := #0|>;
prod := <|carrier := p * R; op := $*; id := #1|> |>
[quotient_ring_add_def] Definition
⊢ ∀r i.
quotient_ring_add r i = <|carrier := R/I; id := I; op := $+ |>
[quotient_ring_def] Definition
⊢ ∀r i.
r / i =
<|carrier := R/I; sum := quotient_ring_add r i;
prod := quotient_ring_mult r i|>
[quotient_ring_mult_def] Definition
⊢ ∀r i.
quotient_ring_mult r i =
<|carrier := R/I; id := #1 ∘ I; op := $* |>
[recordtype_ring_seldef_carrier_def] Definition
⊢ ∀f m m0. (ring f m m0).carrier = f
[recordtype_ring_seldef_carrier_fupd_def] Definition
⊢ ∀f0 f m m0.
ring f m m0 with carrier updated_by f0 = ring (f0 f) m m0
[recordtype_ring_seldef_prod_def] Definition
⊢ ∀f m m0. (ring f m m0).prod = m0
[recordtype_ring_seldef_prod_fupd_def] Definition
⊢ ∀f0 f m m0. ring f m m0 with prod updated_by f0 = ring f m (f0 m0)
[recordtype_ring_seldef_sum_def] Definition
⊢ ∀f m m0. (ring f m m0).sum = m
[recordtype_ring_seldef_sum_fupd_def] Definition
⊢ ∀f0 f m m0. ring f m m0 with sum updated_by f0 = ring f (f0 m) m0
[ring_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('ring').
(∀a0'.
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR 0 (a0,a1,a2)
(λn. ind_type$BOTTOM)) a0 a1 a2) ⇒
$var$('ring') a0') ⇒
$var$('ring') a0') rep
[ring_associates_def] Definition
⊢ ∀r p q. rassoc p q ⇔ ∃s. unit s ∧ p = s * q
[ring_case_def] Definition
⊢ ∀a0 a1 a2 f. ring_CASE (ring a0 a1 a2) f = f a0 a1 a2
[ring_divides_def] Definition
⊢ ∀r q p. q rdivides p ⇔ ∃s. s ∈ R ∧ p = s * q
[ring_fun_def] Definition
⊢ ∀r f. rfun f ⇔ ∀x. f x ∈ R
[ring_gcd_def] Definition
⊢ ∀r f p q.
rgcd p q =
if p = #0 then q
else if q = #0 then p
else
(let
s =
{a * p + b * q |
(a,b) |
a ∈ R ∧ b ∈ R ∧ 0 < f (a * p + b * q)}
in
CHOICE (preimage f s (MIN_SET (IMAGE f s))))
[ring_homo_image_def] Definition
⊢ ∀f r r_.
ring_homo_image f r r_ =
<|carrier := IMAGE f R; sum := homo_image f r.sum r_.sum;
prod := homo_image f r.prod r_.prod|>
[ring_inj_image_def] Definition
⊢ ∀r f.
ring_inj_image r f =
<|carrier := IMAGE f R;
sum :=
<|carrier := IMAGE f R;
op := (λx y. f (LINV f R x + LINV f R y)); id := f #0|>;
prod :=
<|carrier := IMAGE f R;
op := (λx y. f (LINV f R x * LINV f R y)); id := f #1|> |>
[ring_list_def] Definition
⊢ (∀r. rlist [] ⇔ T) ∧ ∀r h t. rlist (h::t) ⇔ h ∈ R ∧ rlist t
[ring_nonzero_def] Definition
⊢ ∀r. R+ = R DIFF {#0}
[ring_ordering_def] Definition
⊢ ∀r f.
ring_ordering r f ⇔
∀a b. a ∈ R ∧ b ∈ R ∧ b ≠ #0 ⇒ f a ≤ f (a * b)
[ring_prime_def] Definition
⊢ ∀r p.
rprime p ⇔
∀a b.
a ∈ R ∧ b ∈ R ∧ p rdivides a * b ⇒ p rdivides a ∨ p rdivides b
[ring_size_def] Definition
⊢ ∀f a0 a1 a2.
ring_size f (ring a0 a1 a2) =
1 + (monoid_size f a1 + monoid_size f a2)
[ring_sub_def] Definition
⊢ ∀r x y. x − y = x + -y
[ring_sum_def] Definition
⊢ (∀r. rsum [] = #0) ∧ ∀r h t. rsum (h::t) = h + rsum t
[subring_def] Definition
⊢ ∀s r. subring s r ⇔ RingHomo I s r
[symdiff_set_inter_def] Definition
⊢ symdiff_set_inter =
<|carrier := 𝕌(:α -> bool); sum := symdiff_set; prod := set_inter|>
[trivial_integal_domain_def] Definition
⊢ ∀e0 e1.
trivial_integal_domain e0 e1 =
<|carrier := {e0; e1};
sum :=
<|carrier := {e0; e1}; id := e0;
op :=
(λx y. if x = e0 then y else if y = e0 then x else e0)|>;
prod :=
<|carrier := {e0; e1}; id := e1;
op :=
(λx y. if x = e0 then e0 else if y = e0 then e0 else e1)|> |>
[trivial_ring_def] Definition
⊢ ∀z. trivial_ring z =
<|carrier := {z};
sum := <|carrier := {z}; id := z; op := (λx y. z)|>;
prod := <|carrier := {z}; id := z; op := (λx y. z)|> |>
[unit_eq_def] Definition
⊢ ∀r x y. x =~ y ⇔ ∃u. unit u ∧ x = u * y
[EXISTS_ring] Theorem
⊢ ∀P. (∃r. P r) ⇔ ∃f m0 m. P <|carrier := f; sum := m0; prod := m|>
[FORALL_ring] Theorem
⊢ ∀P. (∀r. P r) ⇔ ∀f m0 m. P <|carrier := f; sum := m0; prod := m|>
[LIST_REL_ring_associates_product] Theorem
⊢ Ring r ⇒
∀l1 l2.
LIST_REL rassoc l1 l2 ∧ set l2 ⊆ R ⇒
rassoc (GBAG r.prod (LIST_TO_BAG l1))
(GBAG r.prod (LIST_TO_BAG l2))
[WHILE_RULE_PRE_POST] Theorem
⊢ (∀x. Invariant x ∧ Guard x ⇒ f (Cmd x) < f x) ∧
(∀x. Precond x ⇒ Invariant x) ∧
(∀x. Invariant x ∧ ¬Guard x ⇒ Postcond x) ∧
HOARE_SPEC (λx. Invariant x ∧ Guard x) Cmd Invariant ⇒
HOARE_SPEC Precond (WHILE Guard Cmd) Postcond
[ZN_1_exp] Theorem
⊢ ∀n k. (ZN 1).prod.exp n k = 0
[ZN_card] Theorem
⊢ ∀n. CARD (ZN n).carrier = n
[ZN_char] Theorem
⊢ ∀n. 0 < n ⇒ char (ZN n) = n
[ZN_coprime_euler_element] Theorem
⊢ ∀m n. 1 < m ∧ coprime m n ⇒ n MOD m ∈ Euler m
[ZN_coprime_exp_mod] Theorem
⊢ ∀m n.
0 < m ∧ coprime m n ⇒
∀k. n ** k MOD m = n ** (k MOD ordz m n) MOD m
[ZN_coprime_invertible] Theorem
⊢ ∀m n. 1 < m ∧ coprime m n ⇒ Unit (ZN m) (n MOD m)
[ZN_coprime_order] Theorem
⊢ ∀m n.
0 < m ∧ coprime m n ⇒
0 < ordz m n ∧ n ** ordz m n MOD m = 1 MOD m
[ZN_coprime_order_alt] Theorem
⊢ ∀m n. 1 < m ∧ coprime m n ⇒ 0 < ordz m n ∧ n ** ordz m n MOD m = 1
[ZN_coprime_order_divides_phi] Theorem
⊢ ∀m n. 0 < m ∧ coprime m n ⇒ ordz m n divides phi m
[ZN_coprime_order_divides_totient] Theorem
⊢ ∀m n. 0 < m ∧ coprime m n ⇒ ordz m n divides totient m
[ZN_coprime_order_gt_1] Theorem
⊢ ∀m n. 1 < m ∧ 1 < n MOD m ∧ coprime m n ⇒ 1 < ordz m n
[ZN_coprime_order_lt] Theorem
⊢ ∀m n. 1 < m ∧ coprime m n ⇒ ordz m n < m
[ZN_eval] Theorem
⊢ ∀n. (ZN n).carrier = count n ∧ (ZN n).sum = add_mod n ∧
(ZN n).prod = times_mod n
[ZN_exp] Theorem
⊢ ∀n. 0 < n ⇒ ∀x k. (ZN n).prod.exp x k = x ** k MOD n
[ZN_finite] Theorem
⊢ ∀n. FINITE (ZN n).carrier
[ZN_finite_ring] Theorem
⊢ ∀n. 0 < n ⇒ FiniteRing (ZN n)
[ZN_ids] Theorem
⊢ ∀n. 0 < n ⇒ (ZN n).sum.id = 0 ∧ (ZN n).prod.id = 1 MOD n
[ZN_ids_alt] Theorem
⊢ ∀n. 1 < n ⇒ (ZN n).sum.id = 0 ∧ (ZN n).prod.id = 1
[ZN_invertibles] Theorem
⊢ ∀n. 1 < n ⇒ Invertibles (ZN n).prod = Estar n
[ZN_invertibles_finite_group] Theorem
⊢ ∀n. 0 < n ⇒ FiniteGroup (Invertibles (ZN n).prod)
[ZN_invertibles_group] Theorem
⊢ ∀n. 0 < n ⇒ Group (Invertibles (ZN n).prod)
[ZN_invertibles_order] Theorem
⊢ ∀m n. 0 < m ⇒ order (Invertibles (ZN m).prod) (n MOD m) = ordz m n
[ZN_mult_inv_coprime] Theorem
⊢ ∀n. 0 < n ⇒ ∀x y. (x * y) MOD n = 1 ⇒ coprime x n
[ZN_mult_inv_coprime_iff] Theorem
⊢ ∀n. 1 < n ⇒ ∀x. coprime x n ⇔ ∃y. (x * y) MOD n = 1
[ZN_not_coprime] Theorem
⊢ ∀m n. 0 < m ∧ gcd m n ≠ 1 ⇒ ∀k. 0 < k ⇒ n ** k MOD m ≠ 1
[ZN_num] Theorem
⊢ ∀n. 0 < n ⇒ ∀k. (ZN n).sum.exp 1 k = k MOD n
[ZN_num_0] Theorem
⊢ ∀n c. 0 < n ⇒ (ZN n).sum.exp 0 c = 0
[ZN_num_1] Theorem
⊢ ∀n. (ZN n).sum.exp (ZN n).prod.id 1 = 1 MOD n
[ZN_num_mod] Theorem
⊢ ∀n c. 0 < n ⇒ (ZN n).sum.exp (ZN n).prod.id c = c MOD n
[ZN_order_0] Theorem
⊢ ∀n. 0 < n ⇒ ordz n 0 = if n = 1 then 1 else 0
[ZN_order_1] Theorem
⊢ ∀n. 0 < n ⇒ ordz n 1 = 1
[ZN_order_divides_exp] Theorem
⊢ ∀m n k. 1 < m ∧ 0 < k ⇒ (n ** k MOD m = 1 ⇔ ordz m n divides k)
[ZN_order_divides_phi] Theorem
⊢ ∀m n. 0 < m ∧ 0 < ordz m n ⇒ ordz m n divides phi m
[ZN_order_divides_tops_index] Theorem
⊢ ∀n j k.
1 < n ∧ 0 < j ∧ 1 < k ⇒ (k divides tops n j ⇔ ordz k n divides j)
[ZN_order_divisibility] Theorem
⊢ ∀m n. 0 < m ⇒ m divides tops n (ordz m n)
[ZN_order_eq_0] Theorem
⊢ ∀m n. 0 < m ⇒ (ordz m n = 0 ⇔ gcd m n ≠ 1)
[ZN_order_eq_0_iff] Theorem
⊢ ∀m n. 1 < m ⇒ (ordz m n = 0 ⇔ ∀k. 0 < k ⇒ n ** k MOD m ≠ 1)
[ZN_order_eq_0_test] Theorem
⊢ ∀m n. 1 < m ⇒ (ordz m n = 0 ⇔ ∀j. 0 < j ∧ j < m ⇒ n ** j MOD m ≠ 1)
[ZN_order_eq_1] Theorem
⊢ ∀m n. 0 < m ⇒ (ordz m n = 1 ⇔ n MOD m = 1 MOD m)
[ZN_order_eq_1_alt] Theorem
⊢ ∀m n. 1 < m ⇒ (ordz m n = 1 ⇔ n MOD m = 1)
[ZN_order_eq_1_by_prime_factors] Theorem
⊢ ∀m n.
0 < m ∧ coprime m n ∧ (∀p. prime p ∧ p divides n ⇒ ordz m p = 1) ⇒
ordz m n = 1
[ZN_order_gt_1_property] Theorem
⊢ ∀m n.
0 < m ∧ 1 < ordz m n ⇒ ∃p. prime p ∧ p divides n ∧ 1 < ordz m p
[ZN_order_le] Theorem
⊢ ∀m n. 0 < m ⇒ ordz m n ≤ m
[ZN_order_le_tops_index] Theorem
⊢ ∀n j k. 1 < n ∧ 0 < j ∧ 1 < k ∧ k divides tops n j ⇒ ordz k n ≤ j
[ZN_order_lt] Theorem
⊢ ∀k n m. 0 < k ∧ k < m ⇒ ordz k n < m
[ZN_order_minimal] Theorem
⊢ ∀m n k. 0 < m ∧ 0 < k ∧ k < ordz m n ⇒ n ** k MOD m ≠ 1
[ZN_order_mod] Theorem
⊢ ∀m n. 0 < m ⇒ ordz m (n MOD m) = ordz m n
[ZN_order_mod_1] Theorem
⊢ ∀n. ordz 1 n = 1
[ZN_order_nonzero] Theorem
⊢ ∀m n. 0 < m ⇒ (ordz m n ≠ 0 ⇔ coprime m n)
[ZN_order_nonzero_iff] Theorem
⊢ ∀m n. 1 < m ⇒ (ordz m n ≠ 0 ⇔ ∃k. 0 < k ∧ n ** k MOD m = 1)
[ZN_order_property] Theorem
⊢ ∀m n. 0 < m ⇒ n ** ordz m n MOD m = 1 MOD m
[ZN_order_property_alt] Theorem
⊢ ∀m n. 1 < m ⇒ n ** ordz m n MOD m = 1
[ZN_order_test_1] Theorem
⊢ ∀m n k.
1 < m ∧ 0 < k ⇒
(ordz m n = k ⇔
n ** k MOD m = 1 ∧ ∀j. 0 < j ∧ j < k ⇒ n ** j MOD m ≠ 1)
[ZN_order_test_2] Theorem
⊢ ∀m n k.
1 < m ∧ 0 < k ⇒
(ordz m n = k ⇔
n ** k MOD m = 1 ∧
∀j. 0 < j ∧ j < k ∧ j divides phi m ⇒ n ** j MOD m ≠ 1)
[ZN_order_test_3] Theorem
⊢ ∀m n k.
1 < m ∧ 0 < k ⇒
(ordz m n = k ⇔
k divides phi m ∧ n ** k MOD m = 1 ∧
∀j. 0 < j ∧ j < k ∧ j divides phi m ⇒ n ** j MOD m ≠ 1)
[ZN_order_test_4] Theorem
⊢ ∀m n k.
1 < m ⇒
(ordz m n = k ⇔
n ** k MOD m = 1 ∧
∀j. 0 < j ∧ j < (if k = 0 then m else k) ⇒ n ** j MOD m ≠ 1)
[ZN_order_test_propery] Theorem
⊢ ∀m n k.
1 < m ∧ 0 < k ∧ n ** k MOD m = 1 ∧
(∀j. 0 < j ∧ j < k ∧ j divides phi m ⇒ n ** j MOD m ≠ 1) ⇒
∀j. 0 < j ∧ j < k ∧ ¬(j divides phi m) ⇒
ordz m n = k ∨ n ** j MOD m ≠ 1
[ZN_order_upper] Theorem
⊢ ∀m n. 0 < m ⇒ ordz m n ≤ phi m
[ZN_order_with_coprime_1] Theorem
⊢ ∀m n. 1 < n ∧ coprime m n ∧ 1 < ordz m n ⇒ 1 < m
[ZN_order_with_coprime_2] Theorem
⊢ ∀m n k.
1 < m ∧ m divides n ∧ 1 < ordz k m ∧ coprime k n ⇒ 1 < n ∧ 1 < k
[ZN_property] Theorem
⊢ ∀n. (∀x. x ∈ (ZN n).carrier ⇔ x < n) ∧ (ZN n).sum.id = 0 ∧
(ZN n).prod.id = (if n = 1 then 0 else 1) ∧
(∀x y. (ZN n).sum.op x y = (x + y) MOD n) ∧
(∀x y. (ZN n).prod.op x y = (x * y) MOD n) ∧
FINITE (ZN n).carrier ∧ CARD (ZN n).carrier = n
[ZN_ring] Theorem
⊢ ∀n. 0 < n ⇒ Ring (ZN n)
[ZN_to_ZN_element] Theorem
⊢ ∀n m x. 0 < m ∧ x ∈ (ZN n).carrier ⇒ x MOD m ∈ (ZN m).carrier
[ZN_to_ZN_prod_monoid_homo] Theorem
⊢ ∀n m.
0 < n ∧ m divides n ⇒
MonoidHomo (λx. x MOD m) (ZN n).prod (ZN m).prod
[ZN_to_ZN_ring_homo] Theorem
⊢ ∀n m. 0 < n ∧ m divides n ⇒ RingHomo (λx. x MOD m) (ZN n) (ZN m)
[ZN_to_ZN_sum_group_homo] Theorem
⊢ ∀n m.
0 < n ∧ m divides n ⇒
GroupHomo (λx. x MOD m) (ZN n).sum (ZN m).sum
[ZP_finite] Theorem
⊢ ∀p. FINITE (ZP p).carrier
[ZP_finite_integral_domain] Theorem
⊢ ∀p. prime p ⇒ FiniteIntegralDomain (ZP p)
[ZP_integral_domain] Theorem
⊢ ∀p. prime p ⇒ IntegralDomain (ZP p)
[Z_add_abelian_group] Theorem
⊢ AbelianGroup Z_add
[Z_add_group] Theorem
⊢ Group Z_add
[Z_add_inv] Theorem
⊢ ∀z. z ∈ Z_add.carrier ⇒ Z_add.inv z = -z
[Z_euclid_ring] Theorem
⊢ EuclideanRing Z Num
[Z_ideal_map_bij] Theorem
⊢ ∀n. 0 < n ⇒
BIJ (λj. coset Z.sum (&j) (Z* n).sum.carrier) (ZN n).carrier
(Z / Z* n).carrier
[Z_ideal_map_element] Theorem
⊢ ∀n j.
0 < n ∧ j ∈ (ZN n).carrier ⇒
coset Z.sum (&j) (Z* n).sum.carrier ∈ (Z / Z* n).carrier
[Z_ideal_map_group_homo] Theorem
⊢ ∀n. 0 < n ⇒
GroupHomo (λj. coset Z.sum (&j) (Z* n).sum.carrier) (ZN n).sum
(Z / Z* n).sum
[Z_ideal_map_monoid_homo] Theorem
⊢ ∀n. 0 < n ⇒
MonoidHomo (λj. coset Z.sum (&j) (Z* n).sum.carrier)
(ZN n).prod (Z / Z* n).prod
[Z_ideal_sum_group] Theorem
⊢ ∀n. Group (Z* n).sum
[Z_ideal_sum_normal] Theorem
⊢ ∀n. (Z* n).sum << Z.sum
[Z_ideal_sum_subgroup] Theorem
⊢ ∀n. (Z* n).sum ≤ Z.sum
[Z_ideal_thm] Theorem
⊢ ∀n. Z* n << Z
[Z_mult_abelian_monoid] Theorem
⊢ AbelianMonoid Z_mult
[Z_mult_monoid] Theorem
⊢ Monoid Z_mult
[Z_multiple_less_neg_eq] Theorem
⊢ ∀n x y. 0 < n ∧ x < n ∧ y < n ∧ -&x + &y ∈ Z_multiple n ⇒ x = y
[Z_principal_ideal_ring] Theorem
⊢ PrincipalIdealRing Z
[Z_quotient_iso_ZN] Theorem
⊢ ∀n. 0 < n ⇒
RingIso (λj. coset Z.sum (&j) (Z* n).sum.carrier) (ZN n)
(Z / Z* n)
[Z_ring] Theorem
⊢ Ring Z
[Z_sum_cogen] Theorem
⊢ ∀n. 0 < n ⇒
∀x. x ∈ Z.sum.carrier ⇒
∃y. cogen Z.sum (Z* n).sum
(coset Z.sum x (Z* n).sum.carrier) = x + &n * y
[Z_sum_coset_eq] Theorem
⊢ ∀n. 0 < n ⇒
∀p. coset Z.sum p (Z* n).sum.carrier =
coset Z.sum (p % &n) (Z* n).sum.carrier
[char_eq_0] Theorem
⊢ ∀r. char r = 0 ⇔ ∀n. 0 < n ⇒ ##n ≠ #0
[char_minimal] Theorem
⊢ ∀r. 0 < char r ⇒ ∀n. 0 < n ∧ n < char r ⇒ ##n ≠ #0
[char_property] Theorem
⊢ ∀r. ##(char r) = #0
[compute_ordz_0] Theorem
⊢ ∀n. compute_ordz 0 n = ordz 0 n
[compute_ordz_1] Theorem
⊢ ∀n. compute_ordz 1 n = 1
[compute_ordz_eqn] Theorem
⊢ ∀m n. compute_ordz m n = ordz m n
[compute_ordz_hoare] Theorem
⊢ ∀m n.
1 < m ∧ coprime m n ⇒
HOARE_SPEC (λi. 0 < i ∧ i ≤ ordz m n)
(WHILE (λi. n ** i MOD m ≠ 1) SUC) (λi. i = ordz m n)
[datatype_ring] Theorem
⊢ DATATYPE (record ring carrier sum prod)
[euclid_ring_map] Theorem
⊢ ∀r f. EuclideanRing r f ⇒ ∀x. f x = 0 ⇔ x = #0
[euclid_ring_principal_ideal_ring] Theorem
⊢ ∀r f. EuclideanRing r f ⇒ PrincipalIdealRing r
[euclid_ring_property] Theorem
⊢ ∀r f.
EuclideanRing r f ⇒
∀x y.
x ∈ R ∧ y ∈ R ∧ y ≠ #0 ⇒
∃q t. q ∈ R ∧ t ∈ R ∧ x = q * y + t ∧ f t < f y
[euclid_ring_ring] Theorem
⊢ ∀r f. EuclideanRing r f ⇒ Ring r
[finite_integral_domain_nonzero_group] Theorem
⊢ ∀r. FiniteIntegralDomain r ⇒ Group f*
[finite_integral_domain_nonzero_invertible] Theorem
⊢ ∀r. FiniteIntegralDomain r ⇒ monoid_invertibles r.prod = R+
[finite_integral_domain_nonzero_invertible_alt] Theorem
⊢ ∀r. FiniteIntegralDomain r ⇒ monoid_invertibles f* = F*
[finite_integral_domain_period_exists] Theorem
⊢ ∀r. FiniteIntegralDomain r ⇒ ∀x. x ∈ R+ ⇒ ∃k. 0 < k ∧ x ** k = #1
[finite_ring_add_finite_abelian_group] Theorem
⊢ ∀r. FiniteRing r ⇒ FiniteAbelianGroup r.sum ∧ r.sum.carrier = R
[finite_ring_add_finite_group] Theorem
⊢ ∀r. FiniteRing r ⇒ FiniteGroup r.sum ∧ r.sum.carrier = R
[finite_ring_card_eq_1] Theorem
⊢ ∀r. FiniteRing r ⇒ (CARD R = 1 ⇔ #1 = #0)
[finite_ring_card_pos] Theorem
⊢ ∀r. FiniteRing r ⇒ 0 < CARD R
[finite_ring_card_prime] Theorem
⊢ ∀r. FiniteRing r ∧ prime (CARD R) ⇒ char r = CARD R
[finite_ring_char] Theorem
⊢ ∀r. FiniteRing r ⇒ 0 < char r ∧ char r = order r.sum #1
[finite_ring_char_alt] Theorem
⊢ ∀r. FiniteRing r ⇒
∀n. char r = n ⇔
0 < n ∧ ##n = #0 ∧ ∀m. 0 < m ∧ m < n ⇒ ##m ≠ #0
[finite_ring_char_divides] Theorem
⊢ ∀r. FiniteRing r ⇒ char r divides CARD R
[finite_ring_char_pos] Theorem
⊢ ∀r. FiniteRing r ⇒ 0 < char r
[finite_ring_is_ring] Theorem
⊢ ∀r. FiniteRing r ⇒ Ring r
[finite_ring_mult_finite_abelian_monoid] Theorem
⊢ ∀r. FiniteRing r ⇒ FiniteAbelianMonoid r.prod
[finite_ring_mult_finite_monoid] Theorem
⊢ ∀r. FiniteRing r ⇒ FiniteMonoid r.prod
[homo_ring_by_inj] Theorem
⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ RingHomo f r (homo_ring r f)
[homo_ring_property] Theorem
⊢ ∀r f.
fR = IMAGE f R ∧ (homo_ring r f).sum = homo_group r.sum f ∧
(homo_ring r f).prod = homo_group r.prod f
[homo_ring_ring] Theorem
⊢ ∀r f. Ring r ∧ RingHomo f r (homo_ring r f) ⇒ Ring (homo_ring r f)
[homo_ring_subring] Theorem
⊢ ∀r s f. (r ~r~ s) f ⇒ subring (homo_ring r f) s
[ideal_antisym] Theorem
⊢ ∀r i. i << r ∧ r << i ⇒ i = r
[ideal_carrier_sing] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ (SING I ⇔ i = <#0>)
[ideal_carriers] Theorem
⊢ ∀r i. i << r ⇒ i.sum.carrier = I ∧ i.prod.carrier = I
[ideal_cogen_property] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ gen x ∈ R ∧ gen x ∘ I = x
[ideal_congruence_elements] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ R ⇒ (y ∈ I ⇔ x === y)
[ideal_congruence_equiv] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ $=== equiv_on R
[ideal_congruence_iff_inCoset] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y. x ∈ I ∧ y ∈ I ⇒ (x === y ⇔ inCoset r.sum i.sum x y)
[ideal_congruence_mult] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x === y ⇒ z * x === z * y
[ideal_congruence_refl] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ⇒ x === x
[ideal_congruence_sym] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x === y ⇔ y === x)
[ideal_congruence_trans] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x === y ∧ y === z ⇒ x === z
[ideal_coset_add] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ x ∘ I + y ∘ I = (x + y) ∘ I
[ideal_coset_element] Theorem
⊢ ∀r i x.
Ring r ∧ i << r ∧ x ∈ R ⇒ ∀z. z ∈ x ∘ I ⇔ ∃y. y ∈ I ∧ z = x + y
[ideal_coset_eq] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ (x ∘ I = y ∘ I ⇔ x − y ∈ I)
[ideal_coset_eq_carrier] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ∧ x ∘ I = I ⇔ x ∈ I
[ideal_coset_eq_congruence] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x ∘ I = y ∘ I ⇔ x === y)
[ideal_coset_has_gen_diff] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ⇒ gen (x ∘ I) − x ∈ I
[ideal_coset_mult] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ x ∘ I * y ∘ I = (x * y) ∘ I
[ideal_coset_neg] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ⇒ x ∘ I + -x ∘ I = I
[ideal_coset_of_element] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ⇒ x ∘ I = I
[ideal_coset_property] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x. x ∈ R ⇒ x ∘ I ∈ R/I ∧ gen (x ∘ I) ∘ I = x ∘ I
[ideal_coset_zero] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ #0 ∘ I = I
[ideal_element] Theorem
⊢ ∀r i. i << r ⇒ ∀x. x ∈ I ⇒ x ∈ r.sum.carrier
[ideal_element_property] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ⇒ x ∈ R
[ideal_eq_ideal] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i = j ⇔ I = J)
[ideal_gen_exists] Theorem
⊢ ∀r i.
Ring r ∧ i << r ∧ i ≠ <#0> ⇒
∀f. (∀x. f x = 0 ⇔ x = #0) ⇒
∃p. p ∈ I ∧ p ≠ #0 ∧ ∀z. z ∈ I ∧ z ≠ #0 ⇒ f p ≤ f z
[ideal_gen_minimal] Theorem
⊢ ∀r i.
Ring r ∧ i << r ∧ i ≠ <#0> ⇒
∀f. (∀x. f x = 0 ⇔ x = #0) ⇒
∀z. z ∈ I ⇒ (f z < f (ideal_gen r i f) ⇔ z = #0)
[ideal_has_diff] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x − y ∈ I
[ideal_has_multiple] Theorem
⊢ ∀r i. i << r ⇒ ∀x y. x ∈ I ∧ y ∈ R ⇒ x * y ∈ I
[ideal_has_neg] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ⇒ -x ∈ I
[ideal_has_one] Theorem
⊢ ∀r i. Ring r ∧ i << r ∧ #1 ∈ I ⇒ I = R
[ideal_has_principal_ideal] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀p. p ∈ R ⇒ (p ∈ I ⇔ <p> << i)
[ideal_has_product] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x * y ∈ I
[ideal_has_subgroup] Theorem
⊢ ∀r i. i << r ⇒ i.sum ≤ r.sum
[ideal_has_sum] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x + y ∈ I
[ideal_has_zero] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ #0 ∈ I
[ideal_in_quotient_ring] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ I ∈ R/I
[ideal_ops] Theorem
⊢ ∀r i. i << r ⇒ i.sum.op = $+ ∧ i.prod.op = $*
[ideal_product_property] Theorem
⊢ ∀r i. i << r ⇒ ∀x y. x ∈ I ∧ y ∈ R ⇒ x * y ∈ I ∧ y * x ∈ I
[ideal_property] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x + y ∈ I ∧ x * y ∈ I
[ideal_refl] Theorem
⊢ ∀r. Ring r ⇒ r << r
[ideal_sub_ideal] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i << j ⇔ I ⊆ J)
[ideal_sub_itself] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ i << i
[ideal_subgroup_ideal_sum] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ i.sum ≤ (i + j).sum
[ideal_sum_comm] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ i + j = j + i
[ideal_sum_element] Theorem
⊢ ∀i j x. x ∈ (i + j).carrier ⇔ ∃y z. y ∈ I ∧ z ∈ J ∧ x = y + z
[ideal_sum_group] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ Group (i + j).sum
[ideal_sum_has_ideal] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ i << (i + j)
[ideal_sum_has_ideal_comm] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ j << (i + j)
[ideal_sum_ideal] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i + j) << r
[ideal_sum_sub_ideal] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ ((i + j) << j ⇔ i << j)
[ideal_sum_subgroup] Theorem
⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i + j).sum ≤ r.sum
[ideal_with_one] Theorem
⊢ ∀r. Ring r ⇒ ∀i. i << r ∧ #1 ∈ I ⇔ i = r
[ideal_with_unit] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ∧ unit x ⇒ i = r
[ideal_zero] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ i.sum.id = #0
[integral_domain_char] Theorem
⊢ ∀r. IntegralDomain r ⇒ char r = 0 ∨ prime (char r)
[integral_domain_divides_prime] Theorem
⊢ ∀r p x.
IntegralDomain r ∧ x ∈ R ∧ p ∈ R ∧ p ≠ #0 ∧ rprime p ∧ p ∉ R* ∧
x ∉ R* ∧ x rdivides p ⇒
rassoc x p
[integral_domain_exp_eq] Theorem
⊢ ∀r. IntegralDomain r ⇒
∀x. x ∈ R+ ⇒ ∀m n. m < n ∧ x ** m = x ** n ⇒ x ** (n − m) = #1
[integral_domain_exp_eq_zero] Theorem
⊢ ∀r. IntegralDomain r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** n = #0 ⇔ n ≠ 0 ∧ x = #0
[integral_domain_exp_nonzero] Theorem
⊢ ∀r. IntegralDomain r ⇒ ∀x. x ∈ R+ ⇒ ∀n. x ** n ∈ R+
[integral_domain_is_ring] Theorem
⊢ ∀r. IntegralDomain r ⇒ Ring r
[integral_domain_mult_eq_zero] Theorem
⊢ ∀r. IntegralDomain r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ (x * y = #0 ⇔ x = #0 ∨ y = #0)
[integral_domain_mult_lcancel] Theorem
⊢ ∀r. IntegralDomain r ⇒
∀x y z.
x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x * y = x * z ⇔ x = #0 ∨ y = z)
[integral_domain_mult_nonzero] Theorem
⊢ ∀r. IntegralDomain r ⇒ ∀x y. x ∈ R+ ∧ y ∈ R+ ⇒ x * y ∈ R+
[integral_domain_mult_rcancel] Theorem
⊢ ∀r. IntegralDomain r ⇒
∀x y z.
x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y * x = z * x ⇔ x = #0 ∨ y = z)
[integral_domain_nonzero_monoid] Theorem
⊢ ∀r. IntegralDomain r ⇒ Monoid f*
[integral_domain_nonzero_mult_carrier] Theorem
⊢ ∀r. IntegralDomain r ⇒ F* = R+
[integral_domain_nonzero_mult_is_monoid] Theorem
⊢ ∀r. IntegralDomain r ⇒ Monoid (monoid_of_ring_nonzero_mult r)
[integral_domain_nonzero_mult_property] Theorem
⊢ ∀r. IntegralDomain r ⇒
F* = R+ ∧ f*.id = #1 ∧ f*.op = $* ∧ f*.exp = $**
[integral_domain_nonzero_order] Theorem
⊢ ∀r. IntegralDomain r ⇒ ∀x. order r.prod x = order f* x
[integral_domain_one_ne_zero] Theorem
⊢ ∀r. IntegralDomain r ⇒ #1 ≠ #0
[integral_domain_one_nonzero] Theorem
⊢ ∀r. IntegralDomain r ⇒ #1 ∈ R+
[integral_domain_order_eq_0] Theorem
⊢ ∀r. FiniteIntegralDomain r ⇒ ∀x. x ∈ R ⇒ (order f* x = 0 ⇔ x = #0)
[integral_domain_order_nonzero] Theorem
⊢ ∀r. FiniteIntegralDomain r ⇒ ∀x. x ∈ R+ ⇒ order f* x ≠ 0
[integral_domain_order_zero] Theorem
⊢ ∀r. IntegralDomain r ⇒ order f* #0 = 0
[integral_domain_prime_factors_unique] Theorem
⊢ IntegralDomain r ⇒
∀l1 l2.
(∀m. MEM m l1 ⇒ m ∈ R ∧ rprime m ∧ m ≠ #0 ∧ m ∉ R* ) ∧
(∀m. MEM m l2 ⇒ m ∈ R ∧ rprime m ∧ m ≠ #0 ∧ m ∉ R* ) ∧
rassoc (GBAG r.prod (LIST_TO_BAG l1))
(GBAG r.prod (LIST_TO_BAG l2)) ⇒
∃l3. PERM l2 l3 ∧ LIST_REL rassoc l1 l3
[integral_domain_ring_iso] Theorem
⊢ IntegralDomain r ∧ Ring s ∧ RingIso f r s ⇒ IntegralDomain s
[integral_domain_zero_not_unit] Theorem
⊢ ∀r. IntegralDomain r ⇒ #0 ∉ R*
[integral_domain_zero_product] Theorem
⊢ ∀r. IntegralDomain r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ (x * y = #0 ⇔ x = #0 ∨ y = #0)
[irreducible_associates] Theorem
⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒
∀p s. p ∈ R ∧ unit s ⇒ (atom p ⇔ atom (s * p))
[irreducible_element] Theorem
⊢ ∀r p. atom p ⇒ p ∈ R
[irreducible_factors] Theorem
⊢ ∀r z.
atom z ⇒
z ∈ R+ ∧ z ∉ R* ∧ ∀p. p ∈ R ∧ p rdivides z ⇒ rassoc z p ∨ unit p
[kernel_ideal_element] Theorem
⊢ ∀r r_ f x.
x ∈ (kernel_ideal f r r_).carrier ⇔ x ∈ r.sum.carrier ∧ f x = #0_
[kernel_ideal_gen_add_map] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let
i = kernel_ideal f r r_
in
∀x y.
x ∈ R/I ∧ y ∈ R/I ⇒
f (gen ((gen x + gen y) ∘ I)) = f (gen x) +_ f (gen y))
[kernel_ideal_gen_id_map] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let i = kernel_ideal f r r_ in f (gen (#1 ∘ I)) = #1_)
[kernel_ideal_gen_mult_map] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let
i = kernel_ideal f r r_
in
∀x y.
x ∈ R/I ∧ y ∈ R/I ⇒
f (gen ((gen x * gen y) ∘ I)) = f (gen x) *_ f (gen y))
[kernel_ideal_quotient_bij] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let i = kernel_ideal f r r_ in BIJ (f ∘ gen) R/I (IMAGE f R))
[kernel_ideal_quotient_element_eq] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let
i = kernel_ideal f r r_
in
∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ (gen x − gen y ∈ I ⇔ x = y))
[kernel_ideal_quotient_homo] Theorem
⊢ ∀r s f.
(r ~r~ s) f ⇒
(let
i = kernel_ideal f r s
in
RingHomo (f ∘ gen) (r / i) (ring_homo_image f r s))
[kernel_ideal_quotient_inj] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let i = kernel_ideal f r r_ in INJ (f ∘ gen) R/I (IMAGE f R))
[kernel_ideal_quotient_iso] Theorem
⊢ ∀r s f.
(r ~r~ s) f ⇒
(let
i = kernel_ideal f r s
in
RingIso (f ∘ gen) (r / i) (ring_homo_image f r s))
[kernel_ideal_quotient_surj] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let i = kernel_ideal f r r_ in SURJ (f ∘ gen) R/I (IMAGE f R))
[kernel_ideal_sum_eqn] Theorem
⊢ ∀r s f. (kernel_ideal f r s).sum = kernel_group f r.sum s.sum
[ordz_eval] Theorem
⊢ ∀m n. order (times_mod m) n = compute_ordz m n
[prime_is_irreducible] Theorem
⊢ ∀r p.
IntegralDomain r ∧ p ∈ R ∧ rprime p ∧ p ≠ #0 ∧ p ∉ R* ⇒ atom p
[principal_ideal_element] Theorem
⊢ ∀p x. x ∈ <p>.carrier ⇔ ∃z. z ∈ R ∧ x = p * z
[principal_ideal_element_divides] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ ∀x. x ∈ <p>.carrier ⇔ p rdivides x
[principal_ideal_eq_principal_ideal] Theorem
⊢ ∀r. Ring r ⇒ ∀p q u. p ∈ R ∧ q ∈ R ∧ unit u ∧ p = q * u ⇒ <p> = <q>
[principal_ideal_equal_principal_ideal] Theorem
⊢ ∀r. IntegralDomain r ⇒
∀p q. p ∈ R ∧ q ∈ R ⇒ (<p> = <q> ⇔ ∃u. unit u ∧ p = q * u)
[principal_ideal_group] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ Group <p>.sum
[principal_ideal_has_element] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ p ∈ <p>.carrier
[principal_ideal_has_principal_ideal] Theorem
⊢ ∀r. Ring r ⇒ ∀p q. p ∈ R ∧ q ∈ <p>.carrier ⇒ <q> << <p>
[principal_ideal_ideal] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ <p> << r
[principal_ideal_property] Theorem
⊢ ∀r p.
<p>.carrier = p * R ∧ <p>.sum.carrier = p * R ∧
<p>.prod.carrier = p * R ∧ <p>.sum.op = $+ ∧ <p>.prod.op = $* ∧
<p>.sum.id = #0 ∧ <p>.prod.id = #1
[principal_ideal_ring_atom_is_prime] Theorem
⊢ ∀r. PrincipalIdealRing r ⇒ ∀p. atom p ⇒ rprime p
[principal_ideal_ring_ideal_maximal] Theorem
⊢ ∀r. PrincipalIdealRing r ⇒ ∀p. atom p ⇒ maxi <p>
[principal_ideal_ring_irreducible_is_prime] Theorem
⊢ ∀r. PrincipalIdealRing r ⇒ ∀p. atom p ⇒ rprime p
[principal_ideal_sub_implies_divides] Theorem
⊢ ∀r. Ring r ⇒ ∀p q. p ∈ R ∧ q ∈ R ⇒ (q rdivides p ⇔ <p> << <q>)
[principal_ideal_subgroup] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ <p>.sum ≤ r.sum
[principal_ideal_subgroup_normal] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ <p>.sum << r.sum
[principal_ideal_sum_eq_ideal] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀p. p ∈ I ⇒ <p> + i = i
[principal_ideal_sum_equal_ideal] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀p. p ∈ I ⇔ p ∈ R ∧ <p> + i = i
[quotient_ring_add_abelian_group] Theorem
⊢ ∀r. Ring r ∧ i << r ⇒ AbelianGroup (quotient_ring_add r i)
[quotient_ring_add_assoc] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y z. x ∈ R/I ∧ y ∈ R/I ∧ z ∈ R/I ⇒ x + y + z = x + (y + z)
[quotient_ring_add_comm] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x + y = y + x
[quotient_ring_add_element] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x + y ∈ R/I
[quotient_ring_add_group] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ Group (quotient_ring_add r i)
[quotient_ring_add_id] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ I + x = x
[quotient_ring_add_inv] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ ∃y. y ∈ R/I ∧ y + x = I
[quotient_ring_by_principal_ideal] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ Ring (r / <p>)
[quotient_ring_element] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀z. z ∈ R/I ⇔ ∃x. x ∈ R ∧ z = x ∘ I
[quotient_ring_has_ideal] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ I ∈ R/I
[quotient_ring_homo] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ RingHomo (λx. x ∘ I) r (r / i)
[quotient_ring_homo_kernel] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ kernel (λx. x ∘ I) r.sum (r / i).sum = I
[quotient_ring_homo_kernel_ideal] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
RingHomo (λx. x ∘ I) r (r / i) ∧
kernel_ideal (λx. x ∘ I) r (r / i) = i
[quotient_ring_homo_surj] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ SURJ (λx. x ∘ I) R R/I
[quotient_ring_mult_abelian_monoid] Theorem
⊢ ∀r. Ring r ∧ i << r ⇒ AbelianMonoid (quotient_ring_mult r i)
[quotient_ring_mult_assoc] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y z. x ∈ R/I ∧ y ∈ R/I ∧ z ∈ R/I ⇒ x * y * z = x * (y * z)
[quotient_ring_mult_comm] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x * y = y * x
[quotient_ring_mult_element] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x * y ∈ R/I
[quotient_ring_mult_id] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ #1 ∘ I * x = x ∧ x * #1 ∘ I = x
[quotient_ring_mult_ladd] Theorem
⊢ ∀r i.
Ring r ∧ i << r ⇒
∀x y z. x ∈ R/I ∧ y ∈ R/I ∧ z ∈ R/I ⇒ x * (y + z) = x * y + x * z
[quotient_ring_mult_monoid] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ Monoid (quotient_ring_mult r i)
[quotient_ring_property] Theorem
⊢ ∀r i.
(r / i).carrier = R/I ∧ (r / i).sum = quotient_ring_add r i ∧
(r / i).prod = quotient_ring_mult r i
[quotient_ring_ring] Theorem
⊢ ∀r i. Ring r ∧ i << r ⇒ Ring (r / i)
[quotient_ring_ring_sing] Theorem
⊢ ∀r. Ring r ⇒ (r / r).carrier = {R}
[ring_11] Theorem
⊢ ∀a0 a1 a2 a0' a1' a2'.
ring a0 a1 a2 = ring a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
[ring_Axiom] Theorem
⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (ring a0 a1 a2) = f a0 a1 a2
[ring_accessors] Theorem
⊢ (∀f m m0. (ring f m m0).carrier = f) ∧
(∀f m m0. (ring f m m0).sum = m) ∧ ∀f m m0. (ring f m m0).prod = m0
[ring_accfupds] Theorem
⊢ (∀r f. (r with sum updated_by f).carrier = R) ∧
(∀r f. (r with prod updated_by f).carrier = R) ∧
(∀r f. (r with carrier updated_by f).sum = r.sum) ∧
(∀r f. (r with prod updated_by f).sum = r.sum) ∧
(∀r f. (r with carrier updated_by f).prod = r.prod) ∧
(∀r f. (r with sum updated_by f).prod = r.prod) ∧
(∀r f. (r with carrier updated_by f).carrier = f R) ∧
(∀r f. (r with sum updated_by f).sum = f r.sum) ∧
∀r f. (r with prod updated_by f).prod = f r.prod
[ring_add_abelian_group] Theorem
⊢ ∀r. Ring r ⇒ AbelianGroup r.sum
[ring_add_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + y + z = x + (y + z)
[ring_add_assoc_comm] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + (y + z) = y + (x + z)
[ring_add_char_2] Theorem
⊢ ∀r. Ring r ∧ char r = 2 ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y = x − y
[ring_add_comm] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y = y + x
[ring_add_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y ∈ R
[ring_add_eq_zero] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x + y = #0 ⇔ y = -x)
[ring_add_exp_eqn] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. r.sum.exp x n = x * ##n
[ring_add_group] Theorem
⊢ ∀r. Ring r ⇒
Group r.sum ∧ r.sum.carrier = R ∧
∀x y. x ∈ R ∧ y ∈ R ⇒ x + y = y + x
[ring_add_group_rwt] Theorem
⊢ ∀r. Ring r ⇒ Group r.sum ∧ r.sum.carrier = R
[ring_add_lcancel] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x + y = x + z ⇔ y = z)
[ring_add_lneg] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x + x = #0
[ring_add_lneg_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ y = x + (-x + y) ∧ y = -x + (x + y)
[ring_add_lzero] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #0 + x = x
[ring_add_pair_sub] Theorem
⊢ ∀r. Ring r ⇒
∀x y p q.
x ∈ R ∧ y ∈ R ∧ p ∈ R ∧ q ∈ R ⇒
x + y − (p + q) = x − p + (y − q)
[ring_add_rcancel] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y + x = z + x ⇔ y = z)
[ring_add_rneg] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x + -x = #0
[ring_add_rneg_assoc] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ y = y + -x + x ∧ y = y + x + -x
[ring_add_rzero] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x + #0 = x
[ring_add_sub] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y − y = x
[ring_add_sub_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + y − z = x + (y − z)
[ring_add_sub_comm] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ y + x − y = x
[ring_add_sub_identity] Theorem
⊢ ∀r. Ring r ⇒
∀x y z t.
x ∈ R ∧ y ∈ R ∧ z ∈ R ∧ t ∈ R ⇒
(x + y = z + t ⇔ x − z = t − y)
[ring_add_zero_zero] Theorem
⊢ ∀r. Ring r ⇒ #0 + #0 = #0
[ring_associates_divides] Theorem
⊢ ∀r p q x. Ring r ∧ rassoc p q ∧ q ∈ R ∧ p rdivides x ⇒ q rdivides x
[ring_associates_mult] Theorem
⊢ ∀r p q x.
Ring r ∧ p ∈ R ∧ q ∈ R ∧ x ∈ R ∧ rassoc p q ⇒
rassoc (x * p) (x * q)
[ring_associates_refl] Theorem
⊢ ∀r x. Ring r ∧ x ∈ R ⇒ rassoc x x
[ring_associates_sym] Theorem
⊢ ∀r p q. Ring r ∧ q ∈ R ∧ rassoc p q ⇒ rassoc q p
[ring_associates_trans] Theorem
⊢ ∀r x y z. Ring r ∧ z ∈ R ∧ rassoc x y ∧ rassoc y z ⇒ rassoc x z
[ring_auto_I] Theorem
⊢ ∀r. RingAuto I r
[ring_auto_bij] Theorem
⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f PERMUTES R
[ring_auto_cong] Theorem
⊢ ∀r f1 f2.
Ring r ∧ (∀x. x ∈ R ⇒ f1 x = f2 x) ⇒
(RingAuto f1 r ⇔ RingAuto f2 r)
[ring_auto_element] Theorem
⊢ ∀r f. RingAuto f r ⇒ ∀x. x ∈ R ⇒ f x ∈ R
[ring_auto_ids] Theorem
⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f #0 = #0 ∧ f #1 = #1
[ring_auto_linv_auto] Theorem
⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ RingAuto (LINV f R) r
[ring_auto_one] Theorem
⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f #1 = #1
[ring_auto_zero] Theorem
⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f #0 = #0
[ring_binomial_2] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
(x + y) ** 2 = x ** 2 + ##2 * (x * y) + y ** 2
[ring_binomial_3] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
(x + y) ** 3 =
x ** 3 + ##3 * (x ** 2 * y) + ##3 * (x * y ** 2) + y ** 3
[ring_binomial_4] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
(x + y) ** 4 =
x ** 4 + ##4 * (x ** 3 * y) + ##6 * (x ** 2 * y ** 2) +
##4 * (x * y ** 3) + y ** 4
[ring_binomial_genlist_index_shift] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. GENLIST
((λk. ##(binomial n k) * x ** SUC (n − k) * y ** k) ∘
SUC) n =
GENLIST
(λk. ##(binomial n (SUC k)) * x ** (n − k) * y ** SUC k)
n
[ring_binomial_index_shift] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. (λk. ##(binomial (SUC n) k) * x ** (SUC n − k) * y ** k) ∘
SUC =
(λk.
##(binomial (SUC n) (SUC k)) * x ** (n − k) *
y ** SUC k)
[ring_binomial_term_merge_x] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. (λk. x * k) ∘
(λk. ##(binomial n k) * x ** (n − k) * y ** k) =
(λk. ##(binomial n k) * x ** SUC (n − k) * y ** k)
[ring_binomial_term_merge_y] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. (λk. y * k) ∘
(λk. ##(binomial n k) * x ** (n − k) * y ** k) =
(λk. ##(binomial n k) * x ** (n − k) * y ** SUC k)
[ring_binomial_thm] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. (x + y) ** n =
rsum
(GENLIST (λk. ##(binomial n k) * x ** (n − k) * y ** k)
(SUC n))
[ring_carrier_nonempty] Theorem
⊢ ∀r. Ring r ⇒ R ≠ ∅
[ring_carriers] Theorem
⊢ ∀r. Ring r ⇒ r.sum.carrier = R ∧ r.prod.carrier = R
[ring_case_cong] Theorem
⊢ ∀M M' f.
M = M' ∧
(∀a0 a1 a2. M' = ring a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
ring_CASE M f = ring_CASE M' f'
[ring_case_eq] Theorem
⊢ ring_CASE x f = v ⇔ ∃f' m m0. x = ring f' m m0 ∧ f f' m m0 = v
[ring_char_0] Theorem
⊢ ∀r. Ring r ∧ char r = 0 ⇒ INFINITE R
[ring_char_1] Theorem
⊢ ∀r. Ring r ∧ char r = 1 ⇒ R = {#0}
[ring_char_2_double] Theorem
⊢ ∀r. Ring r ∧ char r = 2 ⇒ ∀x. x ∈ R ⇒ x + x = #0
[ring_char_2_neg_one] Theorem
⊢ ∀r. Ring r ∧ char r = 2 ⇒ -#1 = #1
[ring_char_2_property] Theorem
⊢ ∀r. Ring r ∧ char r = 2 ⇒ #1 + #1 = #0
[ring_char_alt] Theorem
⊢ ∀r. Ring r ⇒
∀n. 0 < n ⇒
(char r = n ⇔ ##n = #0 ∧ ∀m. 0 < m ∧ m < n ⇒ ##m ≠ #0)
[ring_char_divides] Theorem
⊢ ∀r. Ring r ⇒ ∀n. ##n = #0 ⇔ char r divides n
[ring_char_eq_1] Theorem
⊢ ∀r. Ring r ⇒ (char r = 1 ⇔ #1 = #0)
[ring_char_prime] Theorem
⊢ ∀r. Ring r ⇒
(prime (char r) ⇔
1 < char r ∧
∀k. 0 < k ∧ k < char r ⇒ ##(binomial (char r) k) = #0)
[ring_char_prime_endo] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒ RingEndo (λx. x ** char r) r
[ring_component_equality] Theorem
⊢ ∀r1 r2.
r1 = r2 ⇔
r1.carrier = r2.carrier ∧ r1.sum = r2.sum ∧ r1.prod = r2.prod
[ring_divides_associates] Theorem
⊢ ∀r x y p.
Ring r ∧ rassoc x y ∧ p ∈ R ∧ y ∈ R ∧ p rdivides x ⇒ p rdivides y
[ring_divides_by_one] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ #1 rdivides p
[ring_divides_by_unit] Theorem
⊢ ∀r. Ring r ⇒ ∀p t. p ∈ R ∧ unit t ⇒ t rdivides p
[ring_divides_iso] Theorem
⊢ ∀r r_ f.
(r =r= r_) f ⇒
∀p q. p ∈ R ∧ p rdivides q ⇒ ring_divides r_ (f p) (f q)
[ring_divides_le] Theorem
⊢ ∀r f.
EuclideanRing r f ∧ ring_ordering r f ⇒
∀p q. p ∈ R ∧ q ∈ R ∧ p ≠ #0 ∧ q rdivides p ⇒ f q ≤ f p
[ring_divides_refl] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ p rdivides p
[ring_divides_trans] Theorem
⊢ ∀r. Ring r ⇒
∀p q t.
p ∈ R ∧ q ∈ R ∧ t ∈ R ∧ p rdivides q ∧ q rdivides t ⇒
p rdivides t
[ring_divides_zero] Theorem
⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ p rdivides #0
[ring_eq_unit_eq] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ∧ x = y ⇒ x =~ y
[ring_exp_0] Theorem
⊢ ∀x. x ** 0 = #1
[ring_exp_1] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x ** 1 = x
[ring_exp_SUC] Theorem
⊢ ∀x n. x ** SUC n = x * x ** n
[ring_exp_add] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n k. x ** (n + k) = x ** n * x ** k
[ring_exp_add_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n k. x ** n * (x ** k * y) = x ** (n + k) * y
[ring_exp_comm] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** n * x = x * x ** n
[ring_exp_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** n ∈ R
[ring_exp_mod_order] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ∧ 0 < order r.prod x ⇒
∀n. x ** n = x ** (n MOD order r.prod x)
[ring_exp_mult] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n k. x ** (n * k) = (x ** n) ** k
[ring_exp_mult_comm] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀m n. (x ** m) ** n = (x ** n) ** m
[ring_exp_neg] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒ ∀n. -x ** n = if EVEN n then x ** n else -(x ** n)
[ring_exp_small] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒
x ** 0 = #1 ∧ x ** 1 = x ∧ x ** 2 = x * x ∧
x ** 3 = x * x ** 2 ∧ x ** 4 = x * x ** 3 ∧
x ** 5 = x * x ** 4 ∧ x ** 6 = x * x ** 5 ∧
x ** 7 = x * x ** 6 ∧ x ** 8 = x * x ** 7 ∧
x ** 9 = x * x ** 8
[ring_exp_suc] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** SUC n = x ** n * x
[ring_factor_multiple] Theorem
⊢ ∀r. Ring r ⇒
∀p q.
p ∈ R ∧ q ∈ R ∧ (∃k. k ∈ R ∧ p = k * q) ⇒
∀z. z ∈ R ∧ (∃s. s ∈ R ∧ z = s * p) ⇒ ∃t. t ∈ R ∧ z = t * q
[ring_fermat_all] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒ ∀n k. ##n ** char r ** k = ##n
[ring_fermat_thm] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒ ∀n. ##n ** char r = ##n
[ring_first_isomorphism_thm] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
(let
i = kernel_ideal f r r_
in
i << r ∧ ring_homo_image f r r_ ≤ r_ ∧
RingIso (f ∘ gen) (r / i) (ring_homo_image f r r_))
[ring_fn_updates] Theorem
⊢ (∀f0 f m m0.
ring f m m0 with carrier updated_by f0 = ring (f0 f) m m0) ∧
(∀f0 f m m0. ring f m m0 with sum updated_by f0 = ring f (f0 m) m0) ∧
∀f0 f m m0. ring f m m0 with prod updated_by f0 = ring f m (f0 m0)
[ring_freshman_all] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. (x + y) ** char r ** n =
x ** char r ** n + y ** char r ** n
[ring_freshman_all_sub] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. (x − y) ** char r ** n =
x ** char r ** n − y ** char r ** n
[ring_freshman_thm] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒ (x + y) ** char r = x ** char r + y ** char r
[ring_freshman_thm_sub] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒ (x − y) ** char r = x ** char r − y ** char r
[ring_fun_add] Theorem
⊢ ∀r. Ring r ⇒ ∀a b. rfun a ∧ rfun b ⇒ rfun (λk. a k + b k)
[ring_fun_from_ring_fun] Theorem
⊢ ∀r. Ring r ⇒ ∀f. rfun f ⇒ ∀x. x ∈ R ⇒ rfun (λj. f j * x ** j)
[ring_fun_from_ring_fun_exp] Theorem
⊢ ∀r. Ring r ⇒
∀f. rfun f ⇒ ∀x. x ∈ R ⇒ ∀n. rfun (λj. (f j * x ** j) ** n)
[ring_fun_genlist] Theorem
⊢ ∀f. rfun f ⇒ ∀n. rlist (GENLIST f n)
[ring_fun_map] Theorem
⊢ ∀f l. rfun f ⇒ rlist (MAP f l)
[ring_fupdcanon] Theorem
⊢ (∀r g f.
r with <|sum updated_by f; carrier updated_by g|> =
r with <|carrier updated_by g; sum updated_by f|>) ∧
(∀r g f.
r with <|prod updated_by f; carrier updated_by g|> =
r with <|carrier updated_by g; prod updated_by f|>) ∧
∀r g f.
r with <|prod updated_by f; sum updated_by g|> =
r with <|sum updated_by g; prod updated_by f|>
[ring_fupdcanon_comp] Theorem
⊢ ((∀g f. sum_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ sum_fupd f) ∧
∀h g f.
sum_fupd f ∘ carrier_fupd g ∘ h =
carrier_fupd g ∘ sum_fupd f ∘ h) ∧
((∀g f. prod_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ prod_fupd f) ∧
∀h g f.
prod_fupd f ∘ carrier_fupd g ∘ h =
carrier_fupd g ∘ prod_fupd f ∘ h) ∧
(∀g f. prod_fupd f ∘ sum_fupd g = sum_fupd g ∘ prod_fupd f) ∧
∀h g f. prod_fupd f ∘ sum_fupd g ∘ h = sum_fupd g ∘ prod_fupd f ∘ h
[ring_fupdfupds] Theorem
⊢ (∀r g f.
r with <|carrier updated_by f; carrier updated_by g|> =
r with carrier updated_by f ∘ g) ∧
(∀r g f.
r with <|sum updated_by f; sum updated_by g|> =
r with sum updated_by f ∘ g) ∧
∀r g f.
r with <|prod updated_by f; prod updated_by g|> =
r with prod updated_by f ∘ g
[ring_fupdfupds_comp] Theorem
⊢ ((∀g f. carrier_fupd f ∘ carrier_fupd g = carrier_fupd (f ∘ g)) ∧
∀h g f.
carrier_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd (f ∘ g) ∘ h) ∧
((∀g f. sum_fupd f ∘ sum_fupd g = sum_fupd (f ∘ g)) ∧
∀h g f. sum_fupd f ∘ sum_fupd g ∘ h = sum_fupd (f ∘ g) ∘ h) ∧
(∀g f. prod_fupd f ∘ prod_fupd g = prod_fupd (f ∘ g)) ∧
∀h g f. prod_fupd f ∘ prod_fupd g ∘ h = prod_fupd (f ∘ g) ∘ h
[ring_gcd_divides] Theorem
⊢ ∀r f.
EuclideanRing r f ⇒
∀p q. p ∈ R ∧ q ∈ R ⇒ rgcd p q rdivides p ∧ rgcd p q rdivides q
[ring_gcd_element] Theorem
⊢ ∀r f. EuclideanRing r f ⇒ ∀p q. p ∈ R ∧ q ∈ R ⇒ rgcd p q ∈ R
[ring_gcd_is_gcd] Theorem
⊢ ∀r f.
EuclideanRing r f ⇒
∀p q.
p ∈ R ∧ q ∈ R ⇒
rgcd p q rdivides p ∧ rgcd p q rdivides q ∧
∀d. d ∈ R ∧ d rdivides p ∧ d rdivides q ⇒ d rdivides rgcd p q
[ring_gcd_linear] Theorem
⊢ ∀r f.
EuclideanRing r f ⇒
∀p q.
p ∈ R ∧ q ∈ R ⇒ ∃a b. a ∈ R ∧ b ∈ R ∧ rgcd p q = a * p + b * q
[ring_gcd_property] Theorem
⊢ ∀r f.
EuclideanRing r f ⇒
∀p q.
p ∈ R ∧ q ∈ R ⇒
∀d. d ∈ R ∧ d rdivides p ∧ d rdivides q ⇒ d rdivides rgcd p q
[ring_gcd_sym] Theorem
⊢ ∀r f. EuclideanRing r f ⇒ ∀p q. p ∈ R ∧ q ∈ R ⇒ rgcd p q = rgcd q p
[ring_gcd_zero] Theorem
⊢ ∀r f p. rgcd p #0 = p ∧ rgcd #0 p = p
[ring_homo_I_refl] Theorem
⊢ ∀r. RingHomo I r r
[ring_homo_add] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y
[ring_homo_char_divides] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ char r_ divides char r
[ring_homo_compose] Theorem
⊢ ∀r s t f1 f2.
RingHomo f1 r s ∧ RingHomo f2 s t ⇒ RingHomo (f2 ∘ f1) r t
[ring_homo_cong] Theorem
⊢ ∀r r_ f1 f2.
Ring r ∧ Ring r_ ∧ (∀x. x ∈ R ⇒ f1 x = f2 x) ⇒
(RingHomo f1 r r_ ⇔ RingHomo f2 r r_)
[ring_homo_element] Theorem
⊢ ∀r r_ f. RingHomo f r r_ ⇒ ∀x. x ∈ R ⇒ f x ∈ R_
[ring_homo_eq_zero] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ∧ INJ f R R_ ⇒ ∀x. x ∈ R ⇒ (f x = #0_ ⇔ x = #0)
[ring_homo_exp] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. x ∈ R ⇒ ∀n. f (x ** n) = f x **_ n
[ring_homo_ideal_group] Theorem
⊢ ∀r s f. (r ~r~ s) f ⇒ ∀i. i << r ⇒ Group (homo_ideal f r s i).sum
[ring_homo_ideal_ideal] Theorem
⊢ ∀r s f.
Ring r ∧ Ring s ∧ RingHomo f r s ∧ SURJ f R s.carrier ⇒
∀i. i << r ⇒ homo_ideal f r s i << s
[ring_homo_ideal_subgroup] Theorem
⊢ ∀r s f. (r ~r~ s) f ⇒ ∀i. i << r ⇒ (homo_ideal f r s i).sum ≤ s.sum
[ring_homo_ids] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ f #0 = #0_ ∧ f #1 = #1_
[ring_homo_image_bij] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ∧ INJ f R R_ ⇒
BIJ f R (ring_homo_image f r r_).carrier
[ring_homo_image_carrier] Theorem
⊢ ∀r r_ f. (ring_homo_image f r r_).carrier = IMAGE f R
[ring_homo_image_homo] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ RingHomo f r (ring_homo_image f r r_)
[ring_homo_image_is_subring] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ subring (ring_homo_image f r r_) r_
[ring_homo_image_iso] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ∧ INJ f R R_ ⇒ RingIso f r (ring_homo_image f r r_)
[ring_homo_image_ring] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ Ring (ring_homo_image f r r_)
[ring_homo_image_subring] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ring_homo_image f r r_ ≤ r_
[ring_homo_image_subring_subring] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
∀s. Ring s ∧ subring s r ⇒ subring (ring_homo_image f s r_) r_
[ring_homo_image_surj_property] Theorem
⊢ ∀r r_ f.
Ring r ∧ Ring r_ ∧ SURJ f R R_ ⇒
RingIso I r_ (ring_homo_image f r r_)
[ring_homo_inv] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ f ( |/ x) = |/_ (f x)
[ring_homo_kernel_ideal] Theorem
⊢ ∀f r s. (r ~r~ s) f ⇒ kernel_ideal f r s << r
[ring_homo_linv_homo] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ∧ BIJ f R R_ ⇒ RingHomo (LINV f R) r_ r
[ring_homo_mult] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x * y) = f x *_ f y
[ring_homo_neg] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. x ∈ R ⇒ f (-x) = $-_ (f x)
[ring_homo_num] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀n. f (##n) = ##_ #1_ n
[ring_homo_num_nonzero] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒ ∀c. 0 < c ∧ c < char r_ ⇒ ##c ≠ #0 ∧ f (##c) ≠ #0_
[ring_homo_one] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ f #1 = #1_
[ring_homo_one_eq_zero] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ∧ #1 = #0 ⇒ #1_ = #0_
[ring_homo_property] Theorem
⊢ ∀r r_ f.
Ring r ∧ RingHomo f r r_ ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y ∧ f (x * y) = f x *_ f y
[ring_homo_ring_homo_subring] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ subring (ring_homo_image f r r_) r_
[ring_homo_sub] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x − y) = f x -_ f y
[ring_homo_subring_homo] Theorem
⊢ ∀r s r_ f. (r ~r~ r_) f ∧ s ≤ r ⇒ (s ~r~ ring_homo_image f s r_) f
[ring_homo_sum_num_property] Theorem
⊢ ∀r r_ f.
(r ~r~ r_) f ⇒
∀c. 0 < c ∧ c < char r_ ⇒ ##c ≠ #0 ∧ ##_ #1_ c ≠ #0_
[ring_homo_sym] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ∧ BIJ f R R_ ⇒ RingHomo (LINV f R) r_ r
[ring_homo_sym_any] Theorem
⊢ Ring r ∧ Ring s ∧ RingHomo f r s ∧
(∀x. x ∈ s.carrier ⇒ i x ∈ R ∧ f (i x) = x) ∧
(∀x. x ∈ R ⇒ i (f x) = x) ⇒
RingHomo i s r
[ring_homo_trans] Theorem
⊢ ∀r s t f1 f2.
RingHomo f1 r s ∧ RingHomo f2 s t ⇒ RingHomo (f2 ∘ f1) r t
[ring_homo_unit] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ unit_ (f x)
[ring_homo_unit_inv] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ |/_ (f x) = f ( |/ x)
[ring_homo_unit_inv_element] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ |/_ (f x) ∈ R_
[ring_homo_unit_inv_nonzero] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ∧ #1_ ≠ #0_ ⇒ ∀x. unit x ⇒ |/_ (f x) ≠ #0_
[ring_homo_unit_nonzero] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ∧ #1_ ≠ #0_ ⇒ ∀x. unit x ⇒ f x ≠ #0_
[ring_homo_zero] Theorem
⊢ ∀r r_ f. (r ~r~ r_) f ⇒ f #0 = #0_
[ring_induction] Theorem
⊢ ∀P. (∀f m m0. P (ring f m m0)) ⇒ ∀r. P r
[ring_inj_image_alt] Theorem
⊢ ∀r f.
Ring r ⇒
ring_inj_image r f =
<|carrier := IMAGE f R; sum := monoid_inj_image r.sum f;
prod := monoid_inj_image r.prod f|>
[ring_inj_image_carrier] Theorem
⊢ ∀r f. (ring_inj_image r f).carrier = IMAGE f R
[ring_inj_image_prod_abelian_monoid] Theorem
⊢ ∀r f.
Ring r ∧ INJ f R 𝕌(:β) ⇒ AbelianMonoid (ring_inj_image r f).prod
[ring_inj_image_prod_monoid] Theorem
⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Monoid (ring_inj_image r f).prod
[ring_inj_image_prod_monoid_homo] Theorem
⊢ ∀r f.
Ring r ∧ INJ f R 𝕌(:β) ⇒
MonoidHomo f r.prod (ring_inj_image r f).prod
[ring_inj_image_ring] Theorem
⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Ring (ring_inj_image r f)
[ring_inj_image_ring_homo] Theorem
⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ RingHomo f r (ring_inj_image r f)
[ring_inj_image_sum_abelian_group] Theorem
⊢ ∀r f.
Ring r ∧ INJ f R 𝕌(:β) ⇒ AbelianGroup (ring_inj_image r f).sum
[ring_inj_image_sum_group] Theorem
⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Group (ring_inj_image r f).sum
[ring_inj_image_sum_group_homo] Theorem
⊢ ∀r f.
Ring r ∧ INJ f R 𝕌(:β) ⇒
GroupHomo f r.sum (ring_inj_image r f).sum
[ring_inj_image_sum_monoid] Theorem
⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Monoid (ring_inj_image r f).sum
[ring_inv_one] Theorem
⊢ ∀r. Ring r ⇒ |/ #1 = #1
[ring_irreducible_gcd] Theorem
⊢ ∀r f.
EuclideanRing r f ⇒
∀p. p ∈ R ∧ atom p ⇒ ∀q. q ∈ R ⇒ unit (rgcd p q) ∨ p rdivides q
[ring_iso_I_refl] Theorem
⊢ ∀r. RingIso I r r
[ring_iso_add] Theorem
⊢ ∀r r_ f.
(r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y
[ring_iso_bij] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ BIJ f R R_
[ring_iso_card_eq] Theorem
⊢ ∀r r_ f. RingIso f r r_ ∧ FINITE R ⇒ CARD R = CARD R_
[ring_iso_char_eq] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ char r_ = char r
[ring_iso_compose] Theorem
⊢ ∀r s t f1 f2.
RingIso f1 r s ∧ RingIso f2 s t ⇒ RingIso (f2 ∘ f1) r t
[ring_iso_cong] Theorem
⊢ ∀r r_ f1 f2.
Ring r ∧ Ring r_ ∧ (∀x. x ∈ R ⇒ f1 x = f2 x) ⇒
(RingIso f1 r r_ ⇔ RingIso f2 r r_)
[ring_iso_element] Theorem
⊢ ∀r r_ f. RingIso f r r_ ⇒ ∀x. x ∈ R ⇒ f x ∈ R_
[ring_iso_element_unique] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (f x = f y ⇔ x = y)
[ring_iso_eq_one] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ (f x = #1_ ⇔ x = #1)
[ring_iso_eq_zero] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ (f x = #0_ ⇔ x = #0)
[ring_iso_exp] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ ∀n. f (x ** n) = f x **_ n
[ring_iso_ids] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ f #0 = #0_ ∧ f #1 = #1_
[ring_iso_inv] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. unit x ⇒ f ( |/ x) = |/_ (f x)
[ring_iso_inverse] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀y. y ∈ R_ ⇒ ∃x. x ∈ R ∧ y = f x
[ring_iso_inverse_element] Theorem
⊢ ∀r r_ f.
(r =r= r_) f ⇒ ∀y. y ∈ R_ ⇒ LINV f R y ∈ R ∧ y = f (LINV f R y)
[ring_iso_linv_iso] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ RingIso (LINV f R) r_ r
[ring_iso_mult] Theorem
⊢ ∀r r_ f.
(r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x * y) = f x *_ f y
[ring_iso_neg] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ f (-x) = $-_ (f x)
[ring_iso_nonzero] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R+ ⇒ f x ∈ R+_
[ring_iso_num] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀n. f (##n) = ##_ #1_ n
[ring_iso_one] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ f #1 = #1_
[ring_iso_property] Theorem
⊢ ∀r r_ f.
Ring r ∧ RingIso f r r_ ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y ∧ f (x * y) = f x *_ f y
[ring_iso_ring_homo_subring] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ subring (ring_homo_image f r r_) r_
[ring_iso_sub] Theorem
⊢ ∀r r_ f.
(r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x − y) = f x -_ f y
[ring_iso_subring_iso] Theorem
⊢ ∀r s r_ f. (r =r= r_) f ∧ s ≤ r ⇒ (s =r= ring_homo_image f s r_) f
[ring_iso_sym] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ RingIso (LINV f R) r_ r
[ring_iso_sym_any] Theorem
⊢ Ring r ∧ Ring s ∧ RingIso f r s ∧
(∀x. x ∈ s.carrier ⇒ i x ∈ R ∧ f (i x) = x) ∧
(∀x. x ∈ R ⇒ i (f x) = x) ⇒
RingIso i s r
[ring_iso_trans] Theorem
⊢ ∀r s t f1 f2.
RingIso f1 r s ∧ RingIso f2 s t ⇒ RingIso (f2 ∘ f1) r t
[ring_iso_unit] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. unit x ⇒ unit_ (f x)
[ring_iso_zero] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ f #0 = #0_
[ring_list_SNOC] Theorem
⊢ ∀x s. rlist (SNOC x s) ⇔ x ∈ R ∧ rlist s
[ring_list_cons] Theorem
⊢ ∀r h t. rlist (h::t) ⇔ h ∈ R ∧ rlist t
[ring_list_from_genlist] Theorem
⊢ ∀r f. rfun f ⇒ ∀n. rlist (GENLIST f n)
[ring_list_from_genlist_ring_fun] Theorem
⊢ ∀r f. rfun f ⇒ ∀n g. rlist (GENLIST (f ∘ g) n)
[ring_list_front_last] Theorem
⊢ ∀s. rlist (FRONT s) ∧ LAST s ∈ R ⇒ rlist s
[ring_list_gen_from_ring_fun] Theorem
⊢ ∀r. Ring r ⇒
∀f. rfun f ⇒
∀x. x ∈ R ⇒ ∀n. rlist (GENLIST (λj. f j * x ** j) n)
[ring_list_nil] Theorem
⊢ ∀r. rlist [] ⇔ T
[ring_literal_11] Theorem
⊢ ∀f1 m01 m1 f2 m02 m2.
<|carrier := f1; sum := m01; prod := m1|> =
<|carrier := f2; sum := m02; prod := m2|> ⇔
f1 = f2 ∧ m01 = m02 ∧ m1 = m2
[ring_literal_nchotomy] Theorem
⊢ ∀r. ∃f m0 m. r = <|carrier := f; sum := m0; prod := m|>
[ring_mult_abelian_monoid] Theorem
⊢ ∀r. Ring r ⇒ AbelianMonoid r.prod
[ring_mult_add] Theorem
⊢ ∀r. Ring r ⇒
∀z y x.
x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒
x * (y + z) = x * y + x * z ∧ (y + z) * x = y * x + z * x
[ring_mult_add_neg] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒
∀n. ##n * x + -x = if n = 0 then -x else ##(n − 1) * x
[ring_mult_add_neg_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. ##n * x + (-x + y) =
if n = 0 then -x + y else ##(n − 1) * x + y
[ring_mult_add_neg_mult] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒
∀m n.
##m * x + -(##n * x) =
if m < n then -(##(n − m) * x) else ##(m − n) * x
[ring_mult_add_neg_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀m n.
##m * x + (-(##n * x) + y) =
if m < n then -(##(n − m) * x) + y else ##(m − n) * x + y
[ring_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * y * z = x * (y * z)
[ring_mult_assoc_comm] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * (y * z) = y * (x * z)
[ring_mult_comm] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * y = y * x
[ring_mult_divides] Theorem
⊢ ∀r p q x.
Ring r ∧ p * q rdivides x ∧ p ∈ R ∧ q ∈ R ⇒
p rdivides x ∧ q rdivides x
[ring_mult_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * y ∈ R
[ring_mult_exp] Theorem
⊢ ∀r. Ring r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. (x * y) ** n = x ** n * y ** n
[ring_mult_ladd] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y + z) * x = y * x + z * x
[ring_mult_lneg] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -x * y = -(x * y)
[ring_mult_lone] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #1 * x = x
[ring_mult_lsub] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * z − y * z = (x − y) * z
[ring_mult_lzero] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #0 * x = #0
[ring_mult_monoid] Theorem
⊢ ∀r. Ring r ⇒
Monoid r.prod ∧ r.prod.carrier = R ∧
∀x y. x ∈ R ∧ y ∈ R ⇒ x * y = y * x
[ring_mult_monoid_rwt] Theorem
⊢ ∀r. Ring r ⇒ Monoid r.prod ∧ r.prod.carrier = R
[ring_mult_neg_neg] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -x * -y = x * y
[ring_mult_one_one] Theorem
⊢ ∀r. Ring r ⇒ #1 * #1 = #1
[ring_mult_pair_diff] Theorem
⊢ ∀r. Ring r ⇒
∀x y p q.
x ∈ R ∧ y ∈ R ∧ p ∈ R ∧ q ∈ R ⇒
x * y − p * q = (x − p) * y + p * (y − q)
[ring_mult_pair_sub] Theorem
⊢ ∀r. Ring r ⇒
∀x y p q.
x ∈ R ∧ y ∈ R ∧ p ∈ R ∧ q ∈ R ⇒
x * y − p * q = (x − p) * (y − q) + (x − p) * q + p * (y − q)
[ring_mult_radd] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * (y + z) = x * y + x * z
[ring_mult_rneg] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * -y = -(x * y)
[ring_mult_rone] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x * #1 = x
[ring_mult_rsub] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * y − x * z = x * (y − z)
[ring_mult_rzero] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x * #0 = #0
[ring_mult_zero_zero] Theorem
⊢ ∀r. Ring r ⇒ #0 * #0 = #0
[ring_nchotomy] Theorem
⊢ ∀rr. ∃f m m0. rr = ring f m m0
[ring_neg_add] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -(x + y) = -x + -y
[ring_neg_add_comm] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -(x + y) = -y + -x
[ring_neg_add_neg] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x + -x = -(##2 * x)
[ring_neg_add_neg_assoc] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -x + (-x + y) = -(##2 * x) + y
[ring_neg_add_neg_mult] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. -x + -(##n * x) = -(##(n + 1) * x)
[ring_neg_add_neg_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. -x + (-(##n * x) + y) = -(##(n + 1) * x) + y
[ring_neg_char_2] Theorem
⊢ ∀r. Ring r ∧ char r = 2 ⇒ ∀x. x ∈ R ⇒ -x = x
[ring_neg_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x ∈ R
[ring_neg_eq] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (-x = -y ⇔ x = y)
[ring_neg_eq_swap] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (-x = y ⇔ x = -y)
[ring_neg_eq_zero] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ (-x = #0 ⇔ x = #0)
[ring_neg_exp] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒ ∀n. -x ** n = if EVEN n then x ** n else -(x ** n)
[ring_neg_mult] Theorem
⊢ ∀r. Ring r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ -(x * y) = -x * y ∧ -(x * y) = x * -y
[ring_neg_mult_add_neg_mult] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒ ∀m n. -(##m * x) + -(##n * x) = -(##(m + n) * x)
[ring_neg_mult_add_neg_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀m n. -(##m * x) + (-(##n * x) + y) = -(##(m + n) * x) + y
[ring_neg_neg] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ --x = x
[ring_neg_nonzero] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R+ ⇒ -x ∈ R+
[ring_neg_one_eq_one] Theorem
⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ (-#1 = #1 ⇔ char r = 2)
[ring_neg_square] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x ** 2 = x ** 2
[ring_neg_sub] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -(x − y) = y − x
[ring_neg_zero] Theorem
⊢ ∀r. Ring r ⇒ -#0 = #0
[ring_nonzero_element] Theorem
⊢ ∀r x. x ∈ R+ ⇒ x ∈ R
[ring_nonzero_eq] Theorem
⊢ ∀r x. x ∈ R+ ⇔ x ∈ R ∧ x ≠ #0
[ring_nonzero_mult_carrier] Theorem
⊢ ∀r. Ring r ⇒ F* = R+
[ring_num_0] Theorem
⊢ ∀r. ##0 = #0
[ring_num_1] Theorem
⊢ ∀r. Ring r ⇒ ##1 = #1
[ring_num_2] Theorem
⊢ ∀r. Ring r ⇒ ##2 = #1 + #1
[ring_num_SUC] Theorem
⊢ ∀r. Ring r ⇒ ∀n. ##(SUC n) = #1 + ##n
[ring_num_add] Theorem
⊢ ∀r. Ring r ⇒ ∀n k. ##(n + k) = ##n + ##k
[ring_num_add_assoc] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀m n. ##m + (##n + x) = ##(m + n) + x
[ring_num_add_mult] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀m n. ##(m + n) * x = ##m * x + ##n * x
[ring_num_add_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀m n. ##(m + n) * x + y = ##m * x + (##n * x + y)
[ring_num_all_zero] Theorem
⊢ ∀r. Ring r ⇒ #1 = #0 ⇒ ∀c. ##c = #0
[ring_num_char_coprime_nonzero] Theorem
⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ ∀c. coprime c (char r) ⇒ ##c ≠ #0
[ring_num_element] Theorem
⊢ ∀r. Ring r ⇒ ∀n. ##n ∈ R
[ring_num_eq] Theorem
⊢ ∀r. Ring r ⇒ ∀n m. n < char r ∧ m < char r ⇒ (##n = ##m ⇔ n = m)
[ring_num_exp] Theorem
⊢ ∀r. Ring r ⇒ ∀m n. ##m ** n = ##(m ** n)
[ring_num_mod] Theorem
⊢ ∀r. Ring r ∧ 0 < char r ⇒ ∀n. ##n = ##(n MOD char r)
[ring_num_mult] Theorem
⊢ ∀r. Ring r ⇒ ∀m n. ##m * ##n = ##(m * n)
[ring_num_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒ ∀m n x. x ∈ R ⇒ ##m * (##n * x) = ##(m * n) * x
[ring_num_mult_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. ##n * x ∈ R
[ring_num_mult_exp] Theorem
⊢ ∀r. Ring r ⇒ ∀k m n. ##k * ##m ** n = ##(k * m ** n)
[ring_num_mult_neg] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. -(##n * x) = ##n * -x
[ring_num_mult_radd] Theorem
⊢ ∀r. Ring r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. ##n * (x + y) = ##n * x + ##n * y
[ring_num_mult_small] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒
#0 * x = #0 ∧ #1 * x = x ∧ ##2 * x = x + x ∧
##3 * x = ##2 * x + x
[ring_num_mult_suc] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. ##(SUC n) * x = ##n * x + x
[ring_num_negative] Theorem
⊢ ∀r. Ring r ∧ 0 < char r ⇒ ∀z. ∃y x. y = ##x ∧ y + ##z = #0
[ring_num_one] Theorem
⊢ ∀r. ##1 = #1 + #0
[ring_num_sub] Theorem
⊢ ∀r. Ring r ⇒ ∀n m. m < n ⇒ ##(n − m) = ##n − ##m
[ring_num_suc] Theorem
⊢ ∀r. Ring r ⇒ ∀n. ##(SUC n) = ##n + #1
[ring_one_element] Theorem
⊢ ∀r. Ring r ⇒ #1 ∈ R
[ring_one_eq_zero] Theorem
⊢ ∀r. Ring r ⇒ (#1 = #0 ⇔ R = {#0})
[ring_one_exp] Theorem
⊢ ∀r. Ring r ⇒ ∀n. #1 ** n = #1
[ring_one_unique] Theorem
⊢ ∀r. Ring r ⇒
∀y. y ∈ R ⇒ ((∀x. x ∈ R ⇒ y * x = x ∨ x * y = x) ⇔ y = #1)
[ring_prime_divides_product] Theorem
⊢ ∀r. Ring r ⇒
∀p. p ∈ R ⇒
(rprime p ∧ p ∉ R* ⇔
∀b. FINITE_BAG b ∧ SET_OF_BAG b ⊆ R ∧
p rdivides GBAG r.prod b ⇒
∃x. x ⋲ b ∧ p rdivides x)
[ring_prime_iso] Theorem
⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀p. p ∈ R ∧ rprime p ⇒ ring_prime r_ (f p)
[ring_product_factors_divide] Theorem
⊢ ∀r. Ring r ⇒
∀b. FINITE_BAG b ⇒
SET_OF_BAG b ⊆ R ∧ GBAG r.prod b rdivides x ⇒
∀y. y ⋲ b ⇒ y rdivides x
[ring_single_add_mult] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x + ##n * x = ##(n + 1) * x
[ring_single_add_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. x + (##n * x + y) = ##(n + 1) * x + y
[ring_single_add_neg_mult] Theorem
⊢ ∀r. Ring r ⇒
∀x. x ∈ R ⇒
∀n. x + -(##n * x) = if n = 0 then x else -(##(n − 1) * x)
[ring_single_add_neg_mult_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒
∀n. x + (-(##n * x) + y) =
if n = 0 then x + y else -(##(n − 1) * x) + y
[ring_single_add_single] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x + x = ##2 * x
[ring_single_add_single_assoc] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + (x + y) = ##2 * x + y
[ring_single_mult_exp] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x * x ** n = x ** (n + 1)
[ring_single_mult_exp_assoc] Theorem
⊢ ∀r. Ring r ⇒
∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. x * (x ** n * y) = x ** (n + 1) * y
[ring_single_mult_single] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x * x = x ** 2
[ring_single_mult_single_assoc] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * (x * y) = x ** 2 * y
[ring_sub_add] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x − y + y = x
[ring_sub_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x − y ∈ R
[ring_sub_eq] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ⇒ x − x = #0
[ring_sub_eq_add] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x − y = z ⇔ x = y + z)
[ring_sub_eq_zero] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x − y = #0 ⇔ x = y)
[ring_sub_lcancel] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x − y = x − z ⇔ y = z)
[ring_sub_pair_reduce] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + z − (y + z) = x − y
[ring_sub_rcancel] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y − x = z − x ⇔ y = z)
[ring_sub_zero] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x − #0 = x
[ring_sum_SNOC] Theorem
⊢ ∀r. Ring r ⇒ ∀k s. k ∈ R ∧ rlist s ⇒ rsum (SNOC k s) = rsum s + k
[ring_sum_append] Theorem
⊢ ∀r. Ring r ⇒
∀s t. rlist s ∧ rlist t ⇒ rsum (s ⧺ t) = rsum s + rsum t
[ring_sum_cons] Theorem
⊢ ∀r h t. rsum (h::t) = h + rsum t
[ring_sum_decompose_first] Theorem
⊢ ∀r f n. rsum (GENLIST f (SUC n)) = f 0 + rsum (GENLIST (f ∘ SUC) n)
[ring_sum_decompose_first_last] Theorem
⊢ ∀r. Ring r ⇒
∀f n.
rfun f ∧ 0 < n ⇒
rsum (GENLIST f (SUC n)) =
f 0 + rsum (GENLIST (f ∘ SUC) (PRE n)) + f n
[ring_sum_decompose_last] Theorem
⊢ ∀r. Ring r ⇒
∀f n.
rfun f ⇒ rsum (GENLIST f (SUC n)) = rsum (GENLIST f n) + f n
[ring_sum_element] Theorem
⊢ ∀r. Ring r ⇒ ∀s. rlist s ⇒ rsum s ∈ R
[ring_sum_freshman_all] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒
∀f. rfun f ⇒
∀x. x ∈ R ⇒
∀n k.
rsum (GENLIST (λj. f j * x ** j) n) ** char r ** k =
rsum (GENLIST (λj. (f j * x ** j) ** char r ** k) n)
[ring_sum_freshman_thm] Theorem
⊢ ∀r. Ring r ∧ prime (char r) ⇒
∀f. rfun f ⇒
∀x. x ∈ R ⇒
∀n. rsum (GENLIST (λj. f j * x ** j) n) ** char r =
rsum (GENLIST (λj. (f j * x ** j) ** char r) n)
[ring_sum_fun_zero] Theorem
⊢ ∀r. Ring r ⇒
∀f. rfun f ⇒
∀n. (∀k. 0 < k ∧ k < n ⇒ f k = #0) ⇒
rsum (MAP f (GENLIST SUC (PRE n))) = #0
[ring_sum_genlist_add] Theorem
⊢ ∀r. Ring r ⇒
∀a b.
rfun a ∧ rfun b ⇒
∀n. rsum (GENLIST a n) + rsum (GENLIST b n) =
rsum (GENLIST (λk. a k + b k) n)
[ring_sum_genlist_append] Theorem
⊢ ∀r. Ring r ⇒
∀a b.
rfun a ∧ rfun b ⇒
∀n. rsum (GENLIST a n ⧺ GENLIST b n) =
rsum (GENLIST (λk. a k + b k) n)
[ring_sum_genlist_const] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. rsum (GENLIST (K x) n) = ##n * x
[ring_sum_genlist_sum] Theorem
⊢ ∀r. Ring r ⇒
∀f. rfun f ⇒
∀n m.
rsum (GENLIST f (n + m)) =
rsum (GENLIST f m) + rsum (GENLIST (λk. f (k + m)) n)
[ring_sum_mult] Theorem
⊢ ∀r. Ring r ⇒
∀k s. k ∈ R ∧ rlist s ⇒ k * rsum s = rsum (MAP (λx. k * x) s)
[ring_sum_mult_ladd] Theorem
⊢ ∀r. Ring r ⇒
∀m n s.
m ∈ R ∧ n ∈ R ∧ rlist s ⇒
(m + n) * rsum s =
rsum (MAP (λx. m * x) s) + rsum (MAP (λx. n * x) s)
[ring_sum_nil] Theorem
⊢ ∀r. rsum [] = #0
[ring_sum_sing] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ rsum [x] = x
[ring_sum_zero] Theorem
⊢ ∀r. Ring r ⇒ ∀n. r.sum.exp #0 n = #0
[ring_unit_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ x ∈ R
[ring_unit_has_inv] Theorem
⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ unit ( |/ x)
[ring_unit_inv_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ |/ x ∈ R
[ring_unit_inv_inv] Theorem
⊢ ∀r. Ring r ⇒ ∀u. unit u ⇒ u = |/ ( |/ u)
[ring_unit_inv_nonzero] Theorem
⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ ∀x. unit x ⇒ |/ x ≠ #0
[ring_unit_linv] Theorem
⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ |/ x * x = #1
[ring_unit_linv_inv] Theorem
⊢ ∀r. Ring r ⇒ ∀u v. unit u ∧ v ∈ R ∧ |/ u * v = #1 ⇒ u = v
[ring_unit_linv_unique] Theorem
⊢ ∀r. Ring r ⇒ ∀u v. u ∈ R ∧ unit v ∧ u * v = #1 ⇒ u = |/ v
[ring_unit_mult_eq_unit] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (unit (x * y) ⇔ unit x ∧ unit y)
[ring_unit_mult_unit] Theorem
⊢ ∀r. Ring r ⇒ ∀u v. unit u ∧ unit v ⇒ unit (u * v)
[ring_unit_mult_zero] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. unit x ∧ y ∈ R ⇒ (x * y = #0 ⇔ y = #0)
[ring_unit_neg] Theorem
⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ unit (-x)
[ring_unit_nonzero] Theorem
⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ ∀x. unit x ⇒ x ≠ #0
[ring_unit_one] Theorem
⊢ ∀r. Ring r ⇒ unit #1
[ring_unit_property] Theorem
⊢ ∀r. Ring r ⇒ ∀u. unit u ⇔ u ∈ R ∧ ∃v. v ∈ R ∧ u * v = #1
[ring_unit_rinv] Theorem
⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ x * |/ x = #1
[ring_unit_rinv_inv] Theorem
⊢ ∀r. Ring r ⇒ ∀u v. u ∈ R ∧ unit v ∧ u * |/ v = #1 ⇒ u = v
[ring_unit_rinv_unique] Theorem
⊢ ∀r. Ring r ⇒ ∀u v. unit u ∧ v ∈ R ∧ u * v = #1 ⇒ v = |/ u
[ring_unit_zero] Theorem
⊢ ∀r. Ring r ⇒ (unit #0 ⇔ #1 = #0)
[ring_units_abelain_group] Theorem
⊢ ∀r. Ring r ⇒ AbelianGroup r*
[ring_units_element] Theorem
⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ x ∈ R
[ring_units_group] Theorem
⊢ ∀r. Ring r ⇒ Group r*
[ring_units_has_one] Theorem
⊢ ∀r. Ring r ⇒ unit #1
[ring_units_has_zero] Theorem
⊢ ∀r. Ring r ⇒ (unit #0 ⇔ #1 = #0)
[ring_units_property] Theorem
⊢ ∀r. Ring r ⇒ r*.op = $* ∧ r*.id = #1
[ring_updates_eq_literal] Theorem
⊢ ∀r f m0 m.
r with <|carrier := f; sum := m0; prod := m|> =
<|carrier := f; sum := m0; prod := m|>
[ring_zero_divides] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ (#0 rdivides x ⇔ x = #0)
[ring_zero_element] Theorem
⊢ ∀r. Ring r ⇒ #0 ∈ R
[ring_zero_exp] Theorem
⊢ ∀r. Ring r ⇒ ∀n. #0 ** n = if n = 0 then #1 else #0
[ring_zero_fix] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ (x + x = x ⇔ x = #0)
[ring_zero_sub] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #0 − x = -x
[ring_zero_unique] Theorem
⊢ ∀r. Ring r ⇒
∀x y.
x ∈ R ∧ y ∈ R ⇒ (y + x = x ⇔ y = #0) ∧ (x + y = x ⇔ y = #0)
[subring_I_antisym] Theorem
⊢ ∀r s. subring s r ∧ subring r s ⇒ RingIso I s r
[subring_add] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x y. x ∈ B ∧ y ∈ B ⇒ s.sum.op x y = x + y
[subring_by_subgroup_submonoid] Theorem
⊢ ∀r s.
s ≤ r ⇔
Ring r ∧ Ring s ∧ subgroup s.sum r.sum ∧ submonoid s.prod r.prod
[subring_carrier_antisym] Theorem
⊢ ∀r s. subring s r ∧ R ⊆ B ⇒ RingIso I s r
[subring_carrier_finite] Theorem
⊢ ∀r s. FiniteRing r ∧ subring s r ⇒ FINITE B
[subring_carrier_subset] Theorem
⊢ ∀r s. subring s r ⇒ B ⊆ R
[subring_char] Theorem
⊢ ∀r s. s ≤ r ⇒ char s = char r
[subring_char_divides] Theorem
⊢ ∀r s. s ≤ r ⇒ char r divides char s
[subring_element] Theorem
⊢ ∀r s. subring s r ⇒ ∀x. x ∈ B ⇒ x ∈ R
[subring_element_alt] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x. x ∈ B ⇒ x ∈ R
[subring_exp] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x. x ∈ B ⇒ ∀n. s.prod.exp x n = x ** n
[subring_finite_ring] Theorem
⊢ ∀r s. FiniteRing r ∧ s ≤ r ⇒ FiniteRing s
[subring_homo_homo] Theorem
⊢ ∀r s r_ f. subring s r ∧ RingHomo f r r_ ⇒ RingHomo f s r_
[subring_ids] Theorem
⊢ ∀r s. s ≤ r ⇒ s.sum.id = #0 ∧ s.prod.id = #1
[subring_mult] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x y. x ∈ B ∧ y ∈ B ⇒ s.prod.op x y = x * y
[subring_neg] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x. x ∈ B ⇒ s.sum.inv x = -x
[subring_num] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀n. s.sum.exp s.prod.id n = ##n
[subring_one] Theorem
⊢ ∀r s. s ≤ r ⇒ s.prod.id = #1
[subring_prod_submonoid] Theorem
⊢ ∀r s. subring s r ⇒ submonoid s.prod r.prod
[subring_property] Theorem
⊢ ∀r s.
Ring s ∧ subring s r ⇒
∀x y.
x ∈ B ∧ y ∈ B ⇒ s.sum.op x y = x + y ∧ s.prod.op x y = x * y
[subring_refl] Theorem
⊢ ∀r. subring r r
[subring_ring_iso_compose] Theorem
⊢ ∀r s r_ f. subring s r ∧ RingIso f r r_ ⇒ RingHomo f s r_
[subring_ring_iso_ring_homo_subring] Theorem
⊢ ∀r s r_ f. s ≤ r ∧ (r =r= r_) f ⇒ ring_homo_image f s r_ ≤ r_
[subring_sub] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x y. x ∈ B ∧ y ∈ B ⇒ ring_sub s x y = x − y
[subring_sum_subgroup] Theorem
⊢ ∀r s. subring s r ⇒ subgroup s.sum r.sum
[subring_trans] Theorem
⊢ ∀r s t. subring r s ∧ subring s t ⇒ subring r t
[subring_unit] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x. Unit s x ⇒ unit x
[subring_unit_inv] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x. Unit s x ⇒ Inv s x = |/ x
[subring_unit_inv_element] Theorem
⊢ ∀r s. s ≤ r ⇒ ∀x. Unit s x ⇒ Inv s x ∈ B
[subring_unit_inv_nonzero] Theorem
⊢ ∀r s. s ≤ r ∧ #1 ≠ #0 ⇒ ∀x. Unit s x ⇒ Inv s x ≠ #0
[subring_unit_nonzero] Theorem
⊢ ∀r s. s ≤ r ∧ #1 ≠ #0 ⇒ ∀x. Unit s x ⇒ x ≠ #0
[subring_zero] Theorem
⊢ ∀r s. s ≤ r ⇒ s.sum.id = #0
[symdiff_eval] Theorem
⊢ symdiff_set.carrier = 𝕌(:α -> bool) ∧
(∀x y. symdiff_set.op x y = x ∪ y DIFF x ∩ y) ∧ symdiff_set.id = ∅
[symdiff_set_inter_char] Theorem
⊢ char symdiff_set_inter = 2
[symdiff_set_inter_ring] Theorem
⊢ Ring symdiff_set_inter
[symdiff_univ_univ_eq_empty] Theorem
⊢ symdiff 𝕌(:α) 𝕌(:α) = ∅
[trivial_char] Theorem
⊢ ∀z. char (trivial_ring z) = 1
[trivial_integral_domain] Theorem
⊢ ∀e0 e1.
e0 ≠ e1 ⇒ FiniteIntegralDomain (trivial_integal_domain e0 e1)
[trivial_ring] Theorem
⊢ ∀z. FiniteRing (trivial_ring z)
[trivial_ring_thm] Theorem
⊢ ∀z. Ring (trivial_ring z)
[unit_eq_refl] Theorem
⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x =~ x
[unit_eq_sym] Theorem
⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ∧ x =~ y ⇒ y =~ x
[unit_eq_trans] Theorem
⊢ ∀r. Ring r ⇒
∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ∧ x =~ y ∧ y =~ z ⇒ x =~ z
[zero_ideal_ideal] Theorem
⊢ ∀r. Ring r ⇒ <#0> << r
[zero_ideal_sing] Theorem
⊢ ∀r. Ring r ⇒ <#0>.carrier = {#0}
*)
end
HOL 4, Trindemossen-2