Structure groupTheory
signature groupTheory =
sig
type thm = Thm.thm
(* Definitions *)
val AbelianGroup_def : thm
val CosetPartition_def : thm
val ElGamal_decrypt_def : thm
val ElGamal_encrypt_def : thm
val Estar_def : thm
val FiniteAbelianGroup_def : thm
val FiniteGroup_def : thm
val GFACT_def : thm
val GROUP_IMAGE_def : thm
val Generated_def : thm
val Generated_subset_def : thm
val GroupAuto_def : thm
val GroupEndo_def : thm
val GroupHomo_def : thm
val GroupIso_def : thm
val Group_def : thm
val OP_IMAGE_def : thm
val StabilizerGroup_def : thm
val Subgroup_def : thm
val Zadd_def : thm
val Zstar_def : thm
val act_by_def : thm
val action_def : thm
val add_mod_def : thm
val all_subgroups_def : thm
val cogen_def : thm
val conjugate_def : thm
val conjugate_subgroup_def : thm
val coset_def : thm
val coset_op_def : thm
val cyclic_def : thm
val cyclic_gen_def : thm
val cyclic_generators_def : thm
val cyclic_index_def : thm
val eq_order_def : thm
val excluding_def : thm
val fixed_points_def : thm
val fn_cyclic_group_def : thm
val group_div_def : thm
val group_equiv_def : thm
val group_fun_def : thm
val homo_image_def : thm
val inCoset_def : thm
val including_def : thm
val kernel_def : thm
val kernel_group_def : thm
val left_coset_def : thm
val make_group_def : thm
val mult_mod_def : thm
val multi_orbits_def : thm
val normal_subgroup_def : thm
val orbit_def : thm
val orbits_def : thm
val preimage_group_def : thm
val quotient_group_def : thm
val reach_def : thm
val right_coset_def : thm
val roots_of_unity_def : thm
val sing_orbits_def : thm
val stabilizer_def : thm
val subgroup_big_cross_def : thm
val subgroup_big_intersect_def : thm
val subgroup_cross_def : thm
val subgroup_def : thm
val subset_big_cross_def : thm
val subset_cross_def : thm
val subset_cross_left_right_def : thm
val subset_group_def : thm
val symdiff_def : thm
val symdiff_set_def : thm
val trivial_group_def : thm
(* Theorems *)
val ElGamal_correctness : thm
val Estar_alt : thm
val Estar_card : thm
val Estar_card_alt : thm
val Estar_carrier : thm
val Estar_carrier_alt : thm
val Estar_element : thm
val Estar_eval : thm
val Estar_exp : thm
val Estar_finite : thm
val Estar_finite_abelian_group : thm
val Estar_finite_group : thm
val Estar_group : thm
val Estar_id : thm
val Estar_inv : thm
val Estar_inv_compute : thm
val Estar_property : thm
val Euler_Fermat_alt : thm
val Euler_Fermat_eqn : thm
val Euler_Fermat_thm : thm
val Fermat_little_eqn : thm
val Fermat_little_thm : thm
val FiniteAbelianGroup_def_alt : thm
val GFACT_element : thm
val GFACT_identity : thm
val GITSET_AS_ITSET : thm
val GPROD_SET_AS_GROUP_IMAGE : thm
val GPROD_SET_IMAGE : thm
val GPROD_SET_REDUCTION : thm
val GPROD_SET_REDUCTION_INSERT : thm
val Generated_subset_exp : thm
val Generated_subset_gen : thm
val Generated_subset_group : thm
val Generated_subset_has_set : thm
val Generated_subset_property : thm
val Generated_subset_subgroup : thm
val Generated_subset_subset : thm
val Invertibles_inv : thm
val Lagrange_identity : thm
val Lagrange_identity_alt : thm
val Lagrange_thm : thm
val OP_IMAGE_EMPTY : thm
val OP_IMAGE_SING : thm
val OP_IMAGE_THM : thm
val PRIME_2 : thm
val PRIME_3 : thm
val PRIME_5 : thm
val PRIME_7 : thm
val SURJ_IMAGE_PREIMAGE : thm
val Subgroup_homo_homo : thm
val Subgroup_subgroup : thm
val Zadd_card : thm
val Zadd_carrier : thm
val Zadd_carrier_alt : thm
val Zadd_element : thm
val Zadd_eval : thm
val Zadd_exp : thm
val Zadd_finite : thm
val Zadd_finite_abelian_group : thm
val Zadd_finite_group : thm
val Zadd_group : thm
val Zadd_id : thm
val Zadd_inv : thm
val Zadd_inv_compute : thm
val Zadd_property : thm
val Zstar_card : thm
val Zstar_carrier : thm
val Zstar_carrier_alt : thm
val Zstar_element : thm
val Zstar_eval : thm
val Zstar_exp : thm
val Zstar_finite : thm
val Zstar_finite_abelian_group : thm
val Zstar_finite_group : thm
val Zstar_group : thm
val Zstar_id : thm
val Zstar_inv : thm
val Zstar_inv_compute : thm
val Zstar_inverse : thm
val Zstar_inverse_compute : thm
val Zstar_property : thm
val abelian_group_is_abelian_monoid : thm
val abelian_group_order_common : thm
val abelian_group_order_common_coprime : thm
val abelian_monoid_invertible_excluding : thm
val abelian_subgroup_abelian : thm
val abelian_subgroup_cross_finite : thm
val abelian_subgroup_cross_subgroup : thm
val action_closure : thm
val action_compose : thm
val action_id : thm
val action_match_condition : thm
val action_match_condition_alt : thm
val action_reachable_coset : thm
val action_reachable_coset_alt : thm
val action_reverse : thm
val action_to_orbit_surj : thm
val action_trans : thm
val add_mod_abelian_group : thm
val add_mod_card : thm
val add_mod_carrier : thm
val add_mod_carrier_alt : thm
val add_mod_cylic : thm
val add_mod_element : thm
val add_mod_eval : thm
val add_mod_exp : thm
val add_mod_finite : thm
val add_mod_finite_abelian_group : thm
val add_mod_finite_group : thm
val add_mod_group : thm
val add_mod_id : thm
val add_mod_inv : thm
val add_mod_inv_compute : thm
val add_mod_order_1 : thm
val add_mod_property : thm
val all_subgroups_element : thm
val all_subgroups_finite : thm
val all_subgroups_has_gen_id : thm
val all_subgroups_subset : thm
val bij_corres : thm
val carrier_card_by_coset_partition : thm
val carrier_card_by_subgroup_coset_partition : thm
val cogen_coset_element : thm
val cogen_element : thm
val cogen_of_subgroup : thm
val conjugate_subgroup_group : thm
val conjugate_subgroup_subgroup : thm
val corres_thm : thm
val coset_alt : thm
val coset_cogen_property : thm
val coset_element : thm
val coset_empty : thm
val coset_homo_group_iso_quotient_group : thm
val coset_id_eq_subgroup : thm
val coset_partition_card : thm
val coset_partition_element : thm
val coset_partition_element_card : thm
val coset_partition_eq_coset_image : thm
val coset_property : thm
val count_formula : thm
val cyclic_element : thm
val cyclic_element_by_gen : thm
val cyclic_element_in_generated : thm
val cyclic_eq_order_partition : thm
val cyclic_eq_order_partition_alt : thm
val cyclic_eq_order_partition_by_card : thm
val cyclic_finite_alt : thm
val cyclic_finite_has_order_divisor : thm
val cyclic_gen_element : thm
val cyclic_gen_order : thm
val cyclic_gen_power_order : thm
val cyclic_generated_by_gen : thm
val cyclic_generated_group : thm
val cyclic_generators_card : thm
val cyclic_generators_coprimes_bij : thm
val cyclic_generators_element : thm
val cyclic_generators_finite : thm
val cyclic_generators_gen_cofactor_eq_orders : thm
val cyclic_generators_nonempty : thm
val cyclic_generators_subset : thm
val cyclic_group : thm
val cyclic_group_abelian : thm
val cyclic_group_comm : thm
val cyclic_image_ord_is_divisors : thm
val cyclic_index_exists : thm
val cyclic_iso_gen : thm
val cyclic_orders_card : thm
val cyclic_orders_nonempty : thm
val cyclic_orders_partition : thm
val cyclic_subgroup_condition : thm
val cyclic_subgroup_cyclic : thm
val cyclic_uroots_cyclic : thm
val cyclic_uroots_has_primitive : thm
val element_coset_property : thm
val eq_order_equiv : thm
val eq_order_is_feq_order : thm
val fermat_little : thm
val fermat_little_alt : thm
val fermat_little_thm : thm
val fermat_roots : thm
val finite_abelian_Fermat : thm
val finite_abelian_group_is_finite_abelian_monoid : thm
val finite_cyclic_group_add_mod_bij : thm
val finite_cyclic_group_add_mod_homo : thm
val finite_cyclic_group_add_mod_iso : thm
val finite_cyclic_group_bij : thm
val finite_cyclic_group_existence : thm
val finite_cyclic_group_homo : thm
val finite_cyclic_group_iso : thm
val finite_cyclic_group_uniqueness : thm
val finite_cyclic_index_add : thm
val finite_cyclic_index_property : thm
val finite_cyclic_index_unique : thm
val finite_group_Fermat : thm
val finite_group_card_pos : thm
val finite_group_exp_not_distinct : thm
val finite_group_exp_period_exists : thm
val finite_group_is_finite_monoid : thm
val finite_group_is_group : thm
val finite_group_is_monoid : thm
val finite_group_order : thm
val finite_group_primitive_property : thm
val finite_homo_image : thm
val finite_monoid_invertibles_is_finite_group : thm
val finite_subgroup_carrier_finite : thm
val finite_subgroup_finite_group : thm
val fixed_points_element : thm
val fixed_points_element_element : thm
val fixed_points_finite : thm
val fixed_points_orbit_iff_sing : thm
val fixed_points_orbit_sing : thm
val fixed_points_subset : thm
val fn_cyclic_group_alt : thm
val fn_cyclic_group_carrier : thm
val fn_cyclic_group_finite_abelian_group : thm
val fn_cyclic_group_finite_group : thm
val fn_cyclic_group_group : thm
val fn_cyclic_group_id : thm
val generated_Fermat : thm
val generated_carrier : thm
val generated_carrier_as_image : thm
val generated_carrier_has_id : thm
val generated_element : thm
val generated_exp : thm
val generated_finite_group : thm
val generated_gen_element : thm
val generated_group : thm
val generated_group_card : thm
val generated_group_finite : thm
val generated_id_carrier : thm
val generated_id_subgroup : thm
val generated_image_subset_all_subgroups : thm
val generated_image_subset_power_set : thm
val generated_property : thm
val generated_subgroup : thm
val generated_subset : thm
val group_all_invertible : thm
val group_alt : thm
val group_assoc : thm
val group_auto_I : thm
val group_auto_bij : thm
val group_auto_compose : thm
val group_auto_element : thm
val group_auto_exp : thm
val group_auto_id : thm
val group_auto_is_monoid_auto : thm
val group_auto_linv_auto : thm
val group_auto_order : thm
val group_carrier_nonempty : thm
val group_comm_exp : thm
val group_comm_exp_exp : thm
val group_comm_op_exp : thm
val group_coset_eq_itself : thm
val group_coset_is_permutation : thm
val group_def_alt : thm
val group_def_by_inverse : thm
val group_div_cancel : thm
val group_div_element : thm
val group_div_lsame : thm
val group_div_pair : thm
val group_div_rsame : thm
val group_excluding_exp : thm
val group_excluding_op : thm
val group_excluding_property : thm
val group_exp_0 : thm
val group_exp_1 : thm
val group_exp_SUC : thm
val group_exp_add : thm
val group_exp_comm : thm
val group_exp_element : thm
val group_exp_eq : thm
val group_exp_eq_condition : thm
val group_exp_equal : thm
val group_exp_inv : thm
val group_exp_mod : thm
val group_exp_mod_order : thm
val group_exp_mult : thm
val group_exp_mult_comm : thm
val group_exp_suc : thm
val group_first_isomorphism_thm : thm
val group_homo_I_refl : thm
val group_homo_compose : thm
val group_homo_cong : thm
val group_homo_element : thm
val group_homo_exp : thm
val group_homo_homo_image_group : thm
val group_homo_id : thm
val group_homo_image_surj_property : thm
val group_homo_inv : thm
val group_homo_is_monoid_homo : thm
val group_homo_monoid_homo : thm
val group_homo_sym : thm
val group_homo_sym_any : thm
val group_homo_trans : thm
val group_id : thm
val group_id_element : thm
val group_id_exp : thm
val group_id_fix : thm
val group_id_id : thm
val group_id_unique : thm
val group_image_as_op_image : thm
val group_image_empty : thm
val group_image_sing : thm
val group_including_excluding_abelian : thm
val group_including_excluding_eqn : thm
val group_including_excluding_group : thm
val group_including_excluding_property : thm
val group_including_property : thm
val group_inj_image_abelian_group : thm
val group_inj_image_excluding_abelian_group : thm
val group_inj_image_excluding_group : thm
val group_inj_image_group : thm
val group_inj_image_group_homo : thm
val group_inv_element : thm
val group_inv_eq : thm
val group_inv_eq_id : thm
val group_inv_eq_swap : thm
val group_inv_exp : thm
val group_inv_id : thm
val group_inv_inv : thm
val group_inv_op : thm
val group_inv_order : thm
val group_inv_thm : thm
val group_is_monoid : thm
val group_iso_I_refl : thm
val group_iso_bij : thm
val group_iso_card_eq : thm
val group_iso_compose : thm
val group_iso_element : thm
val group_iso_exp : thm
val group_iso_group : thm
val group_iso_id : thm
val group_iso_is_monoid_iso : thm
val group_iso_linv_iso : thm
val group_iso_monoid_iso : thm
val group_iso_order : thm
val group_iso_property : thm
val group_iso_sym : thm
val group_iso_trans : thm
val group_lcancel : thm
val group_lid : thm
val group_lid_unique : thm
val group_linv : thm
val group_linv_assoc : thm
val group_linv_unique : thm
val group_lsolve : thm
val group_normal_equiv : thm
val group_normal_equiv_property : thm
val group_normal_equiv_reflexive : thm
val group_normal_equiv_symmetric : thm
val group_normal_equiv_transitive : thm
val group_op_element : thm
val group_op_linv_eq_id : thm
val group_op_linv_eqn : thm
val group_op_rinv_eq_id : thm
val group_op_rinv_eqn : thm
val group_order_cofactor : thm
val group_order_common : thm
val group_order_common_coprime : thm
val group_order_condition : thm
val group_order_divides : thm
val group_order_divides_exp : thm
val group_order_divides_maximal : thm
val group_order_divisor : thm
val group_order_eq_1 : thm
val group_order_exp_cofactor : thm
val group_order_id : thm
val group_order_inv : thm
val group_order_nonzero : thm
val group_order_pos : thm
val group_order_power : thm
val group_order_power_coprime : thm
val group_order_power_eq_0 : thm
val group_order_power_eq_order : thm
val group_order_power_eqn : thm
val group_order_property : thm
val group_order_thm : thm
val group_order_to_generated_bij : thm
val group_order_unique : thm
val group_orders_eq_1 : thm
val group_pair_reduce : thm
val group_rcancel : thm
val group_rid : thm
val group_rid_unique : thm
val group_rinv : thm
val group_rinv_assoc : thm
val group_rinv_unique : thm
val group_rsolve : thm
val group_uroots_group : thm
val group_uroots_has_id : thm
val group_uroots_subgroup : thm
val homo_count_formula : thm
val homo_group_abelian_group : thm
val homo_group_assoc : thm
val homo_group_by_inj : thm
val homo_group_closure : thm
val homo_group_comm : thm
val homo_group_group : thm
val homo_group_id : thm
val homo_group_inv : thm
val homo_image_group : thm
val homo_image_homo_quotient_kernel : thm
val homo_image_iso_quotient_kernel : thm
val homo_image_monoid : thm
val homo_image_subgroup : thm
val homo_image_to_quotient_kernel_bij : thm
val homo_restrict_same_kernel : thm
val image_iso_preimage_quotient : thm
val image_preimage_group : thm
val image_preimage_quotient_same_card : thm
val image_subgroup_subgroup : thm
val inCoset_equiv_on_carrier : thm
val inCoset_refl : thm
val inCoset_sym : thm
val inCoset_trans : thm
val in_coset : thm
val independent_generated_eq : thm
val independent_generator_2_card : thm
val independent_sym : thm
val iso_group_same_card : thm
val kernel_element : thm
val kernel_group_group : thm
val kernel_group_normal : thm
val kernel_group_subgroup : thm
val kernel_property : thm
val kernel_quotient_group : thm
val left_coset_alt : thm
val make_group_property : thm
val monoid_homo_homo_image_monoid : thm
val monoid_inv_id : thm
val monoid_inv_order : thm
val monoid_inv_order_property : thm
val monoid_invertibles_is_group : thm
val mult_mod_abelian_group : thm
val mult_mod_card : thm
val mult_mod_carrier : thm
val mult_mod_carrier_alt : thm
val mult_mod_element : thm
val mult_mod_element_alt : thm
val mult_mod_eval : thm
val mult_mod_exp : thm
val mult_mod_finite : thm
val mult_mod_finite_abelian_group : thm
val mult_mod_finite_group : thm
val mult_mod_group : thm
val mult_mod_id : thm
val mult_mod_inv : thm
val mult_mod_inv_compute : thm
val mult_mod_inverse : thm
val mult_mod_inverse_compute : thm
val mult_mod_property : thm
val multi_orbits_element : thm
val multi_orbits_element_finite : thm
val multi_orbits_element_subset : thm
val multi_orbits_finite : thm
val multi_orbits_subset : thm
val non_fixed_points_card : thm
val non_fixed_points_orbit_not_sing : thm
val normal_cogen_property : thm
val normal_coset_op_property : thm
val normal_coset_property : thm
val normal_coset_property1 : thm
val normal_coset_property2 : thm
val normal_iff_preimage_normal : thm
val normal_preimage_normal : thm
val normal_subgroup_alt : thm
val normal_subgroup_antisym : thm
val normal_subgroup_coset_eq : thm
val normal_subgroup_coset_homo : thm
val normal_subgroup_groups : thm
val normal_subgroup_property : thm
val normal_subgroup_refl : thm
val normal_subgroup_subgroup : thm
val normal_surj_normal : thm
val orbit_alt : thm
val orbit_card_divides_target_card : thm
val orbit_element : thm
val orbit_element_in_target : thm
val orbit_eq_equiv_class : thm
val orbit_eq_orbit : thm
val orbit_finite : thm
val orbit_finite_by_target : thm
val orbit_finite_inj_card_eq : thm
val orbit_has_action_element : thm
val orbit_has_self : thm
val orbit_is_orbits_element : thm
val orbit_sing_fixed_points : thm
val orbit_stabilizer_cosets_bij : thm
val orbit_stabilizer_cosets_bij_alt : thm
val orbit_stabilizer_map_good : thm
val orbit_stabilizer_map_inj : thm
val orbit_stabilizer_thm : thm
val orbit_subset_target : thm
val orbits_alt : thm
val orbits_element : thm
val orbits_element_element : thm
val orbits_element_finite : thm
val orbits_element_is_orbit : thm
val orbits_element_nonempty : thm
val orbits_element_subset : thm
val orbits_eq_partition : thm
val orbits_equal_size_partition_equal_size : thm
val orbits_equal_size_property : thm
val orbits_finite : thm
val orbits_size_factor_partition_factor : thm
val orbits_size_factor_property : thm
val orders_is_feq_class_order : thm
val preimage_cardinality : thm
val preimage_group_group : thm
val preimage_group_property : thm
val preimage_image_subset : thm
val preimage_subgroup_kernel : thm
val preimage_subgroup_subgroup : thm
val prod_image_as_op_image : thm
val quotient_group_assoc : thm
val quotient_group_closure : thm
val quotient_group_group : thm
val quotient_group_id : thm
val quotient_group_inv : thm
val reach_equiv : thm
val reach_refl : thm
val reach_sym : thm
val reach_trans : thm
val right_coset_alt : thm
val roots_of_unity_0 : thm
val roots_of_unity_element : thm
val roots_of_unity_subset : thm
val sing_orbits_card_eqn : thm
val sing_orbits_element : thm
val sing_orbits_element_card : thm
val sing_orbits_element_choice : thm
val sing_orbits_element_finite : thm
val sing_orbits_element_subset : thm
val sing_orbits_finite : thm
val sing_orbits_subset : thm
val sing_orbits_to_fixed_points_bij : thm
val sing_orbits_to_fixed_points_inj : thm
val sing_orbits_to_fixed_points_surj : thm
val stabilizer_as_image : thm
val stabilizer_conjugate : thm
val stabilizer_element : thm
val stabilizer_group_card_divides : thm
val stabilizer_group_carrier : thm
val stabilizer_group_finite_group : thm
val stabilizer_group_group : thm
val stabilizer_group_id : thm
val stabilizer_group_property : thm
val stabilizer_group_subgroup : thm
val stabilizer_has_id : thm
val stabilizer_nonempty : thm
val stabilizer_subset : thm
val subgroup_I_antisym : thm
val subgroup_alt : thm
val subgroup_antisym : thm
val subgroup_big_cross_empty : thm
val subgroup_big_cross_insert : thm
val subgroup_big_cross_thm : thm
val subgroup_big_intersect_element : thm
val subgroup_big_intersect_group : thm
val subgroup_big_intersect_has_id : thm
val subgroup_big_intersect_has_inv : thm
val subgroup_big_intersect_op_element : thm
val subgroup_big_intersect_property : thm
val subgroup_big_intersect_subgroup : thm
val subgroup_big_intersect_subset : thm
val subgroup_carrier_antisym : thm
val subgroup_carrier_nonempty : thm
val subgroup_carrier_subset : thm
val subgroup_conjugate_subgroup_bij : thm
val subgroup_coset_card : thm
val subgroup_coset_card_partition_element : thm
val subgroup_coset_eq : thm
val subgroup_coset_in_partition : thm
val subgroup_coset_nonempty : thm
val subgroup_coset_partition_element : thm
val subgroup_coset_subset : thm
val subgroup_coset_sym : thm
val subgroup_coset_trans : thm
val subgroup_cross_assoc : thm
val subgroup_cross_card : thm
val subgroup_cross_card_eqn : thm
val subgroup_cross_closure_comm_assoc_fun : thm
val subgroup_cross_comm : thm
val subgroup_cross_finite : thm
val subgroup_cross_group : thm
val subgroup_cross_property : thm
val subgroup_cross_self : thm
val subgroup_cross_subgroup : thm
val subgroup_element : thm
val subgroup_eq : thm
val subgroup_eq_carrier : thm
val subgroup_eqn : thm
val subgroup_exp : thm
val subgroup_groups : thm
val subgroup_has_groups : thm
val subgroup_homo_homo : thm
val subgroup_homomorphism : thm
val subgroup_id : thm
val subgroup_incoset_equiv : thm
val subgroup_intersect_group : thm
val subgroup_intersect_has_inv : thm
val subgroup_intersect_inv : thm
val subgroup_intersect_property : thm
val subgroup_intersect_subgroup : thm
val subgroup_inv : thm
val subgroup_inv_closure : thm
val subgroup_is_group : thm
val subgroup_is_submonoid : thm
val subgroup_is_submonoid0 : thm
val subgroup_op : thm
val subgroup_order : thm
val subgroup_order_eqn : thm
val subgroup_property : thm
val subgroup_property_all : thm
val subgroup_refl : thm
val subgroup_reflexive : thm
val subgroup_subset : thm
val subgroup_test_by_cross : thm
val subgroup_thm : thm
val subgroup_to_coset_bij : thm
val subgroup_trans : thm
val subgroup_transitive : thm
val subset_big_cross_empty : thm
val subset_big_cross_insert : thm
val subset_big_cross_thm : thm
val subset_cross_alt : thm
val subset_cross_assoc : thm
val subset_cross_closure_comm_assoc_fun : thm
val subset_cross_comm : thm
val subset_cross_element : thm
val subset_cross_element_iff : thm
val subset_cross_element_preimage_card : thm
val subset_cross_finite : thm
val subset_cross_inv : thm
val subset_cross_partition_property : thm
val subset_cross_preimage_inj : thm
val subset_cross_self : thm
val subset_cross_subset : thm
val subset_cross_to_preimage_cross_bij : thm
val subset_group_exp : thm
val subset_group_order : thm
val subset_group_property : thm
val subset_group_subgroup : thm
val subset_group_submonoid : thm
val subset_preimage_image : thm
val sum_image_as_op_image : thm
val symdiff_set_abelian_group : thm
val symdiff_set_group : thm
val target_card_and_fixed_points_congruence : thm
val target_card_by_fixed_points : thm
val target_card_by_orbit_types : thm
val target_card_by_partition : thm
val target_orbits_disjoint : thm
val target_orbits_union : thm
val trivial_group : thm
val trivial_group_carrier : thm
val trivial_group_id : thm
(*
[monoid] Parent theory of "group"
[AbelianGroup_def] Definition
⊢ ∀g. AbelianGroup g ⇔ Group g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x
[CosetPartition_def] Definition
⊢ ∀g h. CosetPartition g h = partition (inCoset g h) G
[ElGamal_decrypt_def] Definition
⊢ ∀g x a b. ElGamal_decrypt g x (a,b) = |/ (a ** x) * b
[ElGamal_encrypt_def] Definition
⊢ ∀g y h m k. ElGamal_encrypt g y h m k = (y ** k,h ** k * m)
[Estar_def] Definition
⊢ ∀n. Estar n =
<|carrier := Euler n; id := 1; op := (λi j. (i * j) MOD n)|>
[FiniteAbelianGroup_def] Definition
⊢ ∀g. FiniteAbelianGroup g ⇔ AbelianGroup g ∧ FINITE G
[FiniteGroup_def] Definition
⊢ ∀g. FiniteGroup g ⇔ Group g ∧ FINITE G
[GFACT_def] Definition
⊢ ∀g. GFACT g = GPROD_SET g G
[GROUP_IMAGE_def] Definition
⊢ ∀g f s. GPI f s = ITSET (λe acc. f e * acc) s #e
[Generated_def] Definition
⊢ ∀g a.
gen a = <|carrier := {x | ∃k. x = a ** k}; op := $*; id := #e|>
[Generated_subset_def] Definition
⊢ ∀g s.
gen_set s =
<|carrier := BIGINTER (IMAGE (λh. H) {h | h ≤ g ∧ s ⊆ H});
op := $*; id := #e|>
[GroupAuto_def] Definition
⊢ ∀f g. GroupAuto f g ⇔ GroupIso f g g
[GroupEndo_def] Definition
⊢ ∀f g. GroupEndo f g ⇔ GroupHomo f g g
[GroupHomo_def] Definition
⊢ ∀f g h.
GroupHomo f g h ⇔
(∀x. x ∈ G ⇒ f x ∈ h.carrier) ∧
∀x y. x ∈ G ∧ y ∈ G ⇒ f (x * y) = h.op (f x) (f y)
[GroupIso_def] Definition
⊢ ∀f g h. GroupIso f g h ⇔ GroupHomo f g h ∧ BIJ f G h.carrier
[Group_def] Definition
⊢ ∀g. Group g ⇔ Monoid g ∧ G* = G
[OP_IMAGE_def] Definition
⊢ ∀op id f s. OP_IMAGE op id f s = ITSET (λe acc. op (f e) acc) s id
[StabilizerGroup_def] Definition
⊢ ∀f g x.
StabilizerGroup f g x =
<|carrier := stabilizer f g x; op := $*; id := #e|>
[Subgroup_def] Definition
⊢ ∀h g. h ≤ g ⇔ Group h ∧ Group g ∧ H ⊆ G ∧ $o = $*
[Zadd_def] Definition
⊢ ∀n. Z n =
<|carrier := count n; id := 0; op := (λi j. (i + j) MOD n)|>
[Zstar_def] Definition
⊢ ∀p. Z* p =
<|carrier := residue p; id := 1; op := (λi j. (i * j) MOD p)|>
[act_by_def] Definition
⊢ ∀f g x y.
(x ~~ y) f g ⇒ act_by f g x y ∈ G ∧ f (act_by f g x y) x = y
[action_def] Definition
⊢ ∀f g X.
(g act X) f ⇔
∀x. x ∈ X ⇒
(∀a. a ∈ G ⇒ f a x ∈ X) ∧ f #e x = x ∧
∀a b. a ∈ G ∧ b ∈ G ⇒ f a (f b x) = f (a * b) x
[add_mod_def] Definition
⊢ ∀n. add_mod n =
<|carrier := {i | i < n}; id := 0;
op := (λi j. (i + j) MOD n)|>
[all_subgroups_def] Definition
⊢ ∀g. all_subgroups g = {h | h ≤ g}
[cogen_def] Definition
⊢ ∀g h e.
h ≤ g ∧ e ∈ CosetPartition g h ⇒
cogen g h e ∈ G ∧ e = cogen g h e * H
[conjugate_def] Definition
⊢ ∀g a s. conjugate g a s = {a * z * |/ a | z ∈ s}
[conjugate_subgroup_def] Definition
⊢ ∀h g a.
conjugate_subgroup h g a =
<|carrier := conjugate g a H; id := #e; op := $* |>
[coset_def] Definition
⊢ ∀g a X. a * X = IMAGE (λz. a * z) X
[coset_op_def] Definition
⊢ ∀g h x y. x ∘ y = cogen g h x * cogen g h y * H
[cyclic_def] Definition
⊢ ∀g. cyclic g ⇔ Group g ∧ ∃z. z ∈ G ∧ ∀x. x ∈ G ⇒ ∃n. x = z ** n
[cyclic_gen_def] Definition
⊢ ∀g. cyclic g ⇒
cyclic_gen g ∈ G ∧ ∀x. x ∈ G ⇒ ∃n. x = cyclic_gen g ** n
[cyclic_generators_def] Definition
⊢ ∀g. cyclic_generators g = {z | z ∈ G ∧ ord z = CARD G}
[cyclic_index_def] Definition
⊢ ∀g x.
cyclic g ∧ x ∈ G ⇒
x = cyclic_gen g ** cyclic_index g x ∧
(FINITE G ⇒ cyclic_index g x < CARD G)
[eq_order_def] Definition
⊢ ∀g x y. eq_order g x y ⇔ ord x = ord y
[excluding_def] Definition
⊢ ∀g z. g excluding z = <|carrier := G DIFF {z}; op := $*; id := #e|>
[fixed_points_def] Definition
⊢ ∀f g X. fixed_points f g X = {x | x ∈ X ∧ ∀a. a ∈ G ⇒ f a x = x}
[fn_cyclic_group_def] Definition
⊢ ∀e f.
fn_cyclic_group e f =
<|carrier := {x | ∃n. FUNPOW f n e = x}; id := e;
op :=
(λx y.
@z. ∀xi yi.
FUNPOW f xi e = x ∧ FUNPOW f yi e = y ⇒
FUNPOW f (xi + yi) e = z)|>
[group_div_def] Definition
⊢ ∀g x y. x / y = x * |/ y
[group_equiv_def] Definition
⊢ ∀g h x y. x == y ⇔ x / y ∈ H
[group_fun_def] Definition
⊢ ∀g f. gfun f ⇔ ∀x. x ∈ G ⇒ f x ∈ G
[homo_image_def] Definition
⊢ ∀f g h.
homo_image f g h =
<|carrier := IMAGE f G; op := h.op; id := h.id|>
[inCoset_def] Definition
⊢ ∀g h a b. inCoset g h a b ⇔ b ∈ a * H
[including_def] Definition
⊢ ∀g z. g including z = <|carrier := G ∪ {z}; op := $*; id := #e|>
[kernel_def] Definition
⊢ ∀f g h. kernel f g h = preimage f G h.id
[kernel_group_def] Definition
⊢ ∀f g h.
kernel_group f g h =
<|carrier := kernel f g h; id := #e; op := $* |>
[left_coset_def] Definition
⊢ ∀g X a. left_coset g X a = a * X
[make_group_def] Definition
⊢ ∀g s. make_group g s = <|carrier := s; op := $*; id := #e|>
[mult_mod_def] Definition
⊢ ∀p. mult_mod p =
<|carrier := {i | i ≠ 0 ∧ i < p}; id := 1;
op := (λi j. (i * j) MOD p)|>
[multi_orbits_def] Definition
⊢ ∀f g X. multi_orbits f g X = {e | e ∈ orbits f g X ∧ ¬SING e}
[normal_subgroup_def] Definition
⊢ ∀h g. h << g ⇔ h ≤ g ∧ ∀a z. a ∈ G ∧ z ∈ H ⇒ a * z / a ∈ H
[orbit_def] Definition
⊢ ∀f g x. orbit f g x = IMAGE (λa. f a x) G
[orbits_def] Definition
⊢ ∀f g X. orbits f g X = IMAGE (orbit f g) X
[preimage_group_def] Definition
⊢ ∀f g1 g2 h.
preimage_group f g1 g2 h =
<|carrier := PREIMAGE f h ∩ g1.carrier; op := g1.op;
id := g1.id|>
[quotient_group_def] Definition
⊢ ∀g h. g / h = <|carrier := CosetPartition g h; op := $o; id := H|>
[reach_def] Definition
⊢ ∀f g x y. (x ~~ y) f g ⇔ ∃a. a ∈ G ∧ f a x = y
[right_coset_def] Definition
⊢ ∀g X a. X * a = IMAGE (λz. z * a) X
[roots_of_unity_def] Definition
⊢ ∀g n.
uroots n =
<|carrier := {x | x ∈ G ∧ x ** n = #e}; op := $*; id := #e|>
[sing_orbits_def] Definition
⊢ ∀f g X. sing_orbits f g X = {e | e ∈ orbits f g X ∧ SING e}
[stabilizer_def] Definition
⊢ ∀f g x. stabilizer f g x = {a | a ∈ G ∧ f a x = x}
[subgroup_big_cross_def] Definition
⊢ ∀g B. sgbcross B = ITSET $o B (gen #e)
[subgroup_big_intersect_def] Definition
⊢ ∀g. sgbINTER g =
<|carrier := BIGINTER (IMAGE (λh. H) {h | h ≤ g}); op := $*;
id := #e|>
[subgroup_cross_def] Definition
⊢ ∀g h1 h2. h1 ∘ h2 = make_group g (h1.carrier ∘ h2.carrier)
[subgroup_def] Definition
⊢ ∀h g. subgroup h g ⇔ GroupHomo I h g
[subset_big_cross_def] Definition
⊢ ∀g B. ssbcross B = ITSET $o B {#e}
[subset_cross_def] Definition
⊢ ∀g s1 s2. s1 ∘ s2 = {x * y | x ∈ s1 ∧ y ∈ s2}
[subset_cross_left_right_def] Definition
⊢ ∀g s1 s2 z.
z ∈ s1 ∘ s2 ⇒ left z ∈ s1 ∧ right z ∈ s2 ∧ z = left z * right z
[subset_group_def] Definition
⊢ ∀g s. subset_group g s = <|carrier := s; op := $*; id := #e|>
[symdiff_def] Definition
⊢ ∀s1 s2. symdiff s1 s2 = s1 ∪ s2 DIFF s1 ∩ s2
[symdiff_set_def] Definition
⊢ symdiff_set = <|carrier := 𝕌(:α -> bool); id := ∅; op := symdiff|>
[trivial_group_def] Definition
⊢ ∀e. trivial_group e = <|carrier := {e}; id := e; op := (λx y. e)|>
[ElGamal_correctness] Theorem
⊢ ∀g. Group g ⇒
∀(y::G) (h::G) (m::G) k x.
h = y ** x ⇒
ElGamal_decrypt g x (ElGamal_encrypt g y h m k) = m
[Estar_alt] Theorem
⊢ ∀n. Estar n =
<|carrier := {i | 0 < i ∧ i < n ∧ coprime n i}; id := 1;
op := (λi j. (i * j) MOD n)|>
[Estar_card] Theorem
⊢ ∀n. CARD (Estar n).carrier = totient n
[Estar_card_alt] Theorem
⊢ ∀n. 1 < n ⇒ CARD (Estar n).carrier = phi n
[Estar_carrier] Theorem
⊢ ∀n. (Estar n).carrier = Euler n
[Estar_carrier_alt] Theorem
⊢ ∀n. (Estar n).carrier = {i | 0 < i ∧ i < n ∧ coprime n i}
[Estar_element] Theorem
⊢ ∀n x. x ∈ (Estar n).carrier ⇔ 0 < x ∧ x < n ∧ coprime n x
[Estar_eval] Theorem
⊢ ∀n. (Estar n).carrier = Euler n ∧
(∀x y. (Estar n).op x y = (x * y) MOD n) ∧ (Estar n).id = 1
[Estar_exp] Theorem
⊢ ∀n a.
1 < n ∧ a ∈ (Estar n).carrier ⇒
∀k. (Estar n).exp a k = a ** k MOD n
[Estar_finite] Theorem
⊢ ∀n. FINITE (Estar n).carrier
[Estar_finite_abelian_group] Theorem
⊢ ∀n. 1 < n ⇒ FiniteAbelianGroup (Estar n)
[Estar_finite_group] Theorem
⊢ ∀n. 1 < n ⇒ FiniteGroup (Estar n)
[Estar_group] Theorem
⊢ ∀n. 1 < n ⇒ Group (Estar n)
[Estar_id] Theorem
⊢ ∀n. (Estar n).id = 1
[Estar_inv] Theorem
⊢ ∀n a.
1 < n ∧ a < n ∧ coprime n a ⇒
(Estar n).inv a = a ** (totient n − 1) MOD n
[Estar_inv_compute] Theorem
⊢ ∀n a.
(Estar n).inv a =
if 1 < n ∧ a < n ∧ coprime n a then a ** (totient n − 1) MOD n
else FAIL ((Estar n).inv a) bad_element
[Estar_property] Theorem
⊢ ∀n. (Estar n).carrier = Euler n ∧ (Estar n).id = 1 ∧
(∀x y. (Estar n).op x y = (x * y) MOD n) ∧
FINITE (Estar n).carrier ∧ CARD (Estar n).carrier = totient n
[Euler_Fermat_alt] Theorem
⊢ ∀n a. 1 < n ∧ coprime a n ⇒ a ** totient n MOD n = 1
[Euler_Fermat_eqn] Theorem
⊢ ∀n a. 1 < n ∧ a < n ∧ coprime n a ⇒ a ** totient n MOD n = 1
[Euler_Fermat_thm] Theorem
⊢ ∀n a. 1 < n ∧ coprime n a ⇒ a ** totient n MOD n = 1
[Fermat_little_eqn] Theorem
⊢ ∀p a. prime p ⇒ a ** p MOD p = a MOD p
[Fermat_little_thm] Theorem
⊢ ∀p a. prime p ∧ 0 < a ∧ a < p ⇒ a ** (p − 1) MOD p = 1
[FiniteAbelianGroup_def_alt] Theorem
⊢ ∀g. FiniteAbelianGroup g ⇔
FiniteGroup g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x
[GFACT_element] Theorem
⊢ ∀g. FiniteAbelianMonoid g ⇒ GFACT g ∈ G
[GFACT_identity] Theorem
⊢ ∀g a.
FiniteAbelianGroup g ∧ a ∈ G ⇒ GFACT g = a ** CARD G * GFACT g
[GITSET_AS_ITSET] Theorem
⊢ ∀g. (λs b. GITSET g s b) = ITSET (λe acc. e * acc)
[GPROD_SET_AS_GROUP_IMAGE] Theorem
⊢ ∀g. GPROD_SET g = GPI I
[GPROD_SET_IMAGE] Theorem
⊢ ∀g a. Group g ∧ a ∈ G ⇒ GPROD_SET g (a * G) = GPROD_SET g G
[GPROD_SET_REDUCTION] Theorem
⊢ ∀g s.
FiniteAbelianGroup g ∧ s ⊆ G ⇒
∀a::G.
a ** CARD s * GPROD_SET g s * GPROD_SET g (a * (G DIFF s)) =
GPROD_SET g G
[GPROD_SET_REDUCTION_INSERT] Theorem
⊢ ∀g s.
FiniteAbelianGroup g ∧ s ⊆ G ⇒
∀a x::G.
x ∉ s ⇒
a * x * GPROD_SET g (a * (G DIFF (x INSERT s))) =
GPROD_SET g (a * (G DIFF s))
[Generated_subset_exp] Theorem
⊢ ∀g s. (gen_set s).exp = $**
[Generated_subset_gen] Theorem
⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ gen_set (Gen a) = gen a
[Generated_subset_group] Theorem
⊢ ∀g s. Group g ∧ s ⊆ G ⇒ Group (gen_set s)
[Generated_subset_has_set] Theorem
⊢ ∀g s. s ⊆ (gen_set s).carrier
[Generated_subset_property] Theorem
⊢ ∀g s.
(gen_set s).carrier =
BIGINTER (IMAGE (λh. H) {h | h ≤ g ∧ s ⊆ H}) ∧
(gen_set s).op = $* ∧ (gen_set s).id = #e
[Generated_subset_subgroup] Theorem
⊢ ∀g s. Group g ∧ s ⊆ G ⇒ gen_set s ≤ g
[Generated_subset_subset] Theorem
⊢ ∀g s. Group g ∧ s ⊆ G ⇒ (gen_set s).carrier ⊆ G
[Invertibles_inv] Theorem
⊢ ∀g x. Monoid g ∧ x ∈ G* ⇒ (Invertibles g).inv x = |/ x
[Lagrange_identity] Theorem
⊢ ∀g h.
h ≤ g ∧ FINITE G ⇒ CARD G = CARD H * CARD (CosetPartition g h)
[Lagrange_identity_alt] Theorem
⊢ ∀g h.
h ≤ g ∧ FINITE G ⇒
CARD G = CARD H * CARD (partition (left_coset g H) G)
[Lagrange_thm] Theorem
⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ CARD H divides CARD G
[OP_IMAGE_EMPTY] Theorem
⊢ ∀op id f. OP_IMAGE op id f ∅ = id
[OP_IMAGE_SING] Theorem
⊢ ∀op id f x. OP_IMAGE op id f {x} = op (f x) id
[OP_IMAGE_THM] Theorem
⊢ ∀op id f.
OP_IMAGE op id f ∅ = id ∧
(FUN_COMM op f ⇒
∀s. FINITE s ⇒
∀e. OP_IMAGE op id f (e INSERT s) =
op (f e) (OP_IMAGE op id f (s DELETE e)))
[PRIME_2] Theorem
⊢ prime 2
[PRIME_3] Theorem
⊢ prime 3
[PRIME_5] Theorem
⊢ prime 5
[PRIME_7] Theorem
⊢ prime 7
[SURJ_IMAGE_PREIMAGE] Theorem
⊢ ∀f a b. s ⊆ b ∧ SURJ f a b ⇒ IMAGE f (PREIMAGE f s ∩ a) = s
[Subgroup_homo_homo] Theorem
⊢ ∀g h k f. h ≤ g ∧ GroupHomo f g k ⇒ GroupHomo f h k
[Subgroup_subgroup] Theorem
⊢ ∀g h. h ≤ g ⇒ subgroup h g
[Zadd_card] Theorem
⊢ ∀n. CARD (Z n).carrier = n
[Zadd_carrier] Theorem
⊢ ∀n. (Z n).carrier = count n
[Zadd_carrier_alt] Theorem
⊢ ∀n. (Z n).carrier = {i | i < n}
[Zadd_element] Theorem
⊢ ∀n x. x ∈ (Z n).carrier ⇔ x < n
[Zadd_eval] Theorem
⊢ ∀n. (Z n).carrier = count n ∧
(∀x y. (Z n).op x y = (x + y) MOD n) ∧ (Z n).id = 0
[Zadd_exp] Theorem
⊢ ∀n. 0 < n ⇒ ∀x m. (Z n).exp x m = (x * m) MOD n
[Zadd_finite] Theorem
⊢ ∀n. FINITE (Z n).carrier
[Zadd_finite_abelian_group] Theorem
⊢ ∀n. 0 < n ⇒ FiniteAbelianGroup (Z n)
[Zadd_finite_group] Theorem
⊢ ∀n. 0 < n ⇒ FiniteGroup (Z n)
[Zadd_group] Theorem
⊢ ∀n. 0 < n ⇒ Group (Z n)
[Zadd_id] Theorem
⊢ ∀n. (Z n).id = 0
[Zadd_inv] Theorem
⊢ ∀n x. 0 < n ∧ x < n ⇒ (Z n).inv x = (n − x) MOD n
[Zadd_inv_compute] Theorem
⊢ ∀n x.
(Z n).inv x =
if 0 < n ∧ x < n then (n − x) MOD n
else FAIL ((Z n).inv x) bad_element
[Zadd_property] Theorem
⊢ ∀n. (∀x. x ∈ (Z n).carrier ⇔ x < n) ∧ (Z n).id = 0 ∧
(∀x y. (Z n).op x y = (x + y) MOD n) ∧ FINITE (Z n).carrier ∧
CARD (Z n).carrier = n
[Zstar_card] Theorem
⊢ ∀p. 0 < p ⇒ CARD (Z* p).carrier = p − 1
[Zstar_carrier] Theorem
⊢ ∀p. (Z* p).carrier = residue p
[Zstar_carrier_alt] Theorem
⊢ ∀p. (Z* p).carrier = {i | 0 < i ∧ i < p}
[Zstar_element] Theorem
⊢ ∀p x. x ∈ (Z* p).carrier ⇔ 0 < x ∧ x < p
[Zstar_eval] Theorem
⊢ ∀p. (Z* p).carrier = residue p ∧
(∀x y. (Z* p).op x y = (x * y) MOD p) ∧ (Z* p).id = 1
[Zstar_exp] Theorem
⊢ ∀p a.
prime p ∧ a ∈ (Z* p).carrier ⇒ ∀n. (Z* p).exp a n = a ** n MOD p
[Zstar_finite] Theorem
⊢ ∀p. FINITE (Z* p).carrier
[Zstar_finite_abelian_group] Theorem
⊢ ∀p. prime p ⇒ FiniteAbelianGroup (Z* p)
[Zstar_finite_group] Theorem
⊢ ∀p. prime p ⇒ FiniteGroup (Z* p)
[Zstar_group] Theorem
⊢ ∀p. prime p ⇒ Group (Z* p)
[Zstar_id] Theorem
⊢ ∀p. (Z* p).id = 1
[Zstar_inv] Theorem
⊢ ∀p. prime p ⇒
∀x. 0 < x ∧ x < p ⇒
(Z* p).inv x = (Z* p).exp x (order (Z* p) x − 1)
[Zstar_inv_compute] Theorem
⊢ ∀p x.
(Z* p).inv x =
if prime p ∧ 0 < x ∧ x < p then (Z* p).exp x (order (Z* p) x − 1)
else FAIL ((Z* p).inv x) bad_element
[Zstar_inverse] Theorem
⊢ ∀p. prime p ⇒ ∀a. 0 < a ∧ a < p ⇒ (Z* p).inv a = a ** (p − 2) MOD p
[Zstar_inverse_compute] Theorem
⊢ ∀p a.
(Z* p).inv a =
if prime p ∧ 0 < a ∧ a < p then a ** (p − 2) MOD p
else (Z* p).inv a
[Zstar_property] Theorem
⊢ ∀p. (Z* p).carrier = residue p ∧ (Z* p).id = 1 ∧
(∀x y. (Z* p).op x y = (x * y) MOD p) ∧ FINITE (Z* p).carrier ∧
(0 < p ⇒ CARD (Z* p).carrier = p − 1)
[abelian_group_is_abelian_monoid] Theorem
⊢ ∀g. AbelianGroup g ⇒ AbelianMonoid g
[abelian_group_order_common] Theorem
⊢ ∀g. AbelianGroup g ⇒
∀x y.
x ∈ G ∧ y ∈ G ⇒
∃z. z ∈ G ∧ ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y)
[abelian_group_order_common_coprime] Theorem
⊢ ∀g. AbelianGroup g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ coprime (ord x) (ord y) ⇒
∃z. z ∈ G ∧ ord z = ord x * ord y
[abelian_monoid_invertible_excluding] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀z. z ∉ G* ⇒ monoid_invertibles (g excluding z) = G*
[abelian_subgroup_abelian] Theorem
⊢ ∀g h. AbelianGroup g ∧ h ≤ g ⇒ AbelianGroup h
[abelian_subgroup_cross_finite] Theorem
⊢ ∀g. AbelianGroup g ⇒
∀h1 h2.
h1 ≤ g ∧ h2 ≤ g ∧ FiniteGroup h1 ∧ FiniteGroup h2 ⇒
FiniteGroup (h1 ∘ h2)
[abelian_subgroup_cross_subgroup] Theorem
⊢ ∀g. AbelianGroup g ⇒ ∀h1 h2. h1 ≤ g ∧ h2 ≤ g ⇒ h1 ∘ h2 ≤ g
[action_closure] Theorem
⊢ ∀f g X. (g act X) f ⇒ ∀a x. a ∈ G ∧ x ∈ X ⇒ f a x ∈ X
[action_compose] Theorem
⊢ ∀f g X.
(g act X) f ⇒
∀a b x. a ∈ G ∧ b ∈ G ∧ x ∈ X ⇒ f a (f b x) = f (a * b) x
[action_id] Theorem
⊢ ∀f g X. (g act X) f ⇒ ∀x. x ∈ X ⇒ f #e x = x
[action_match_condition] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒
∀a b.
a ∈ G ∧ b ∈ G ⇒ (f a x = f b x ⇔ |/ a * b ∈ stabilizer f g x)
[action_match_condition_alt] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒
∀a b::G. f a x = f b x ⇔ |/ a * b ∈ stabilizer f g x
[action_reachable_coset] Theorem
⊢ ∀f g X x y.
Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ orbit f g x ⇒
act_by f g x y * stabilizer f g x = {a | a ∈ G ∧ f a x = y}
[action_reachable_coset_alt] Theorem
⊢ ∀f g X x y.
Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ orbit f g x ⇒
∀a. a ∈ G ∧ f a x = y ⇒
a * stabilizer f g x = {b | b ∈ G ∧ f b x = y}
[action_reverse] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
∀a x y. a ∈ G ∧ x ∈ X ∧ y ∈ X ∧ f a x = y ⇒ f ( |/ a) y = x
[action_to_orbit_surj] Theorem
⊢ ∀f g X x. (g act X) f ∧ x ∈ X ⇒ SURJ (λa. f a x) G (orbit f g x)
[action_trans] Theorem
⊢ ∀f g X.
(g act X) f ⇒
∀a b x y z.
a ∈ G ∧ b ∈ G ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X ∧ f a x = y ∧ f b y = z ⇒
f (b * a) x = z
[add_mod_abelian_group] Theorem
⊢ ∀n. 0 < n ⇒ AbelianGroup (add_mod n)
[add_mod_card] Theorem
⊢ ∀n. CARD (add_mod n).carrier = n
[add_mod_carrier] Theorem
⊢ ∀n. (add_mod n).carrier = {i | i < n}
[add_mod_carrier_alt] Theorem
⊢ ∀n. (add_mod n).carrier = count n
[add_mod_cylic] Theorem
⊢ ∀n. 0 < n ⇒ cyclic (add_mod n)
[add_mod_element] Theorem
⊢ ∀n x. x ∈ (add_mod n).carrier ⇔ x < n
[add_mod_eval] Theorem
⊢ ∀n. (add_mod n).carrier = {i | i < n} ∧
(∀x y. (add_mod n).op x y = (x + y) MOD n) ∧ (add_mod n).id = 0
[add_mod_exp] Theorem
⊢ ∀n. 0 < n ⇒ ∀x m. (add_mod n).exp x m = (x * m) MOD n
[add_mod_finite] Theorem
⊢ ∀n. FINITE (add_mod n).carrier
[add_mod_finite_abelian_group] Theorem
⊢ ∀n. 0 < n ⇒ FiniteAbelianGroup (add_mod n)
[add_mod_finite_group] Theorem
⊢ ∀n. 0 < n ⇒ FiniteGroup (add_mod n)
[add_mod_group] Theorem
⊢ ∀n. 0 < n ⇒ Group (add_mod n)
[add_mod_id] Theorem
⊢ ∀n. (add_mod n).id = 0
[add_mod_inv] Theorem
⊢ ∀n x. 0 < n ∧ x < n ⇒ (add_mod n).inv x = (n − x) MOD n
[add_mod_inv_compute] Theorem
⊢ ∀n x.
(add_mod n).inv x =
if 0 < n ∧ x < n then (n − x) MOD n
else FAIL ((add_mod n).inv x) bad_element
[add_mod_order_1] Theorem
⊢ ∀n. 1 < n ⇒ order (add_mod n) 1 = n
[add_mod_property] Theorem
⊢ ∀n. (∀x. x ∈ (add_mod n).carrier ⇔ x < n) ∧ (add_mod n).id = 0 ∧
(∀x y. (add_mod n).op x y = (x + y) MOD n) ∧
FINITE (add_mod n).carrier ∧ CARD (add_mod n).carrier = n
[all_subgroups_element] Theorem
⊢ ∀g h. h ∈ all_subgroups g ⇔ h ≤ g
[all_subgroups_finite] Theorem
⊢ ∀g. FiniteGroup g ⇒ FINITE (all_subgroups g)
[all_subgroups_has_gen_id] Theorem
⊢ ∀g. Group g ⇒ gen #e ∈ all_subgroups g
[all_subgroups_subset] Theorem
⊢ ∀g. Group g ⇒ IMAGE (λh. H) (all_subgroups g) ⊆ POW G
[bij_corres] Theorem
⊢ ∀f g1 g2 h1 h2.
Group g1 ∧ Group g2 ∧ h1 ≤ g1 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ∧
SURJ f g1.carrier g2.carrier ∧ kernel f g1 g2 ⊆ h1.carrier ⇒
IMAGE f (PREIMAGE f h2.carrier ∩ g1.carrier) = h2.carrier ∧
PREIMAGE f (IMAGE f h1.carrier) ∩ g1.carrier = h1.carrier
[carrier_card_by_coset_partition] Theorem
⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ CARD G = ∑ CARD (CosetPartition g h)
[carrier_card_by_subgroup_coset_partition] Theorem
⊢ ∀g h.
h ≤ g ∧ FINITE G ⇒ CARD G = ∑ CARD (partition (left_coset g H) G)
[cogen_coset_element] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ G ⇒ cogen g h (x * H) ∈ G
[cogen_element] Theorem
⊢ ∀h g e. h ≤ g ∧ e ∈ CosetPartition g h ⇒ cogen g h e ∈ G
[cogen_of_subgroup] Theorem
⊢ ∀g h. h ≤ g ⇒ cogen g h H * H = H
[conjugate_subgroup_group] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀a. a ∈ G ⇒ Group (conjugate_subgroup h g a)
[conjugate_subgroup_subgroup] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀a::G. conjugate_subgroup h g a ≤ g
[corres_thm] Theorem
⊢ ∀f g1 g2 h1 h2.
Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧
SURJ f g1.carrier g2.carrier ∧ h1 ≤ g1 ∧
kernel f g1 g2 ⊆ h1.carrier ∧ h2 ≤ g2 ⇒
homo_image f h1 g2 ≤ g2 ∧
preimage_group f g1 g2 h2.carrier ≤ g1 ∧
kernel f g1 g2 ⊆ PREIMAGE f h2.carrier ∩ g1.carrier ∧
(h2 << g2 ⇔ preimage_group f g1 g2 h2.carrier << g1) ∧
IMAGE f (PREIMAGE f h2.carrier ∩ g1.carrier) = h2.carrier ∧
PREIMAGE f (IMAGE f h1.carrier) ∩ g1.carrier = h1.carrier ∧
(FiniteGroup g1 ⇒
CARD (preimage_group f g1 g2 h2.carrier).carrier =
CARD h2.carrier * CARD (kernel f g1 g2))
[coset_alt] Theorem
⊢ ∀g a X. a * X = {a * z | z ∈ X}
[coset_cogen_property] Theorem
⊢ ∀h g e. h ≤ g ∧ e ∈ CosetPartition g h ⇒ e = cogen g h e * H
[coset_element] Theorem
⊢ ∀g X a. a ∈ G ⇒ ∀x. x ∈ a * X ⇔ ∃y. y ∈ X ∧ x = a * y
[coset_empty] Theorem
⊢ ∀g a. Group g ∧ a ∈ G ⇒ a * ∅ = ∅
[coset_homo_group_iso_quotient_group] Theorem
⊢ ∀g h. h << g ⇒ GroupIso I (homo_group g (left_coset g H)) (g / h)
[coset_id_eq_subgroup] Theorem
⊢ ∀g h. h ≤ g ⇒ #e * H = H
[coset_partition_card] Theorem
⊢ ∀g h.
h ≤ g ∧ FINITE G ⇒ CARD (CosetPartition g h) = CARD G DIV CARD H
[coset_partition_element] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀e. e ∈ CosetPartition g h ⇔ ∃a. a ∈ G ∧ e = a * H
[coset_partition_element_card] Theorem
⊢ ∀g h.
h ≤ g ∧ FINITE G ⇒ ∀e. e ∈ CosetPartition g h ⇒ CARD e = CARD H
[coset_partition_eq_coset_image] Theorem
⊢ ∀g h. h ≤ g ⇒ CosetPartition g h = IMAGE (left_coset g H) G
[coset_property] Theorem
⊢ ∀g a. Group g ∧ a ∈ G ⇒ ∀X. X ⊆ G ⇒ a * X ⊆ G
[count_formula] Theorem
⊢ ∀g h.
FiniteGroup g ∧ h << g ⇒ CARD G = CARD H * CARD (g / h).carrier
[cyclic_element] Theorem
⊢ ∀g. cyclic g ⇒ ∀x. x ∈ G ⇒ ∃n. x = cyclic_gen g ** n
[cyclic_element_by_gen] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀x. x ∈ G ⇒ ∃n. n < CARD G ∧ x = cyclic_gen g ** n
[cyclic_element_in_generated] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀x. x ∈ G ⇒ x ∈ Gen (cyclic_gen g ** (CARD G DIV ord x))
[cyclic_eq_order_partition] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
partition (eq_order g) G = {orders g n | n | n divides CARD G}
[cyclic_eq_order_partition_alt] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
partition (eq_order g) G =
{orders g n | n | n ∈ divisors (CARD G)}
[cyclic_eq_order_partition_by_card] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
IMAGE CARD (partition (eq_order g) G) =
IMAGE phi (divisors (CARD G))
[cyclic_finite_alt] Theorem
⊢ ∀g. FiniteGroup g ⇒ (cyclic g ⇔ ∃z. z ∈ G ∧ ord z = CARD G)
[cyclic_finite_has_order_divisor] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀n. n divides CARD G ⇒ ∃x. x ∈ G ∧ ord x = n
[cyclic_gen_element] Theorem
⊢ ∀g. cyclic g ⇒ cyclic_gen g ∈ G
[cyclic_gen_order] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒ ord (cyclic_gen g) = CARD G
[cyclic_gen_power_order] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀n. 0 < n ∧ CARD G MOD n = 0 ⇒
ord (cyclic_gen g ** (CARD G DIV n)) = n
[cyclic_generated_by_gen] Theorem
⊢ ∀g. cyclic g ⇒ g = gen (cyclic_gen g)
[cyclic_generated_group] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ cyclic (gen x)
[cyclic_generators_card] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒ CARD (cyclic_generators g) = phi (CARD G)
[cyclic_generators_coprimes_bij] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
BIJ (λj. cyclic_gen g ** j) (coprimes (CARD G))
(cyclic_generators g)
[cyclic_generators_element] Theorem
⊢ ∀g z. z ∈ cyclic_generators g ⇔ z ∈ G ∧ ord z = CARD G
[cyclic_generators_finite] Theorem
⊢ ∀g. FINITE G ⇒ FINITE (cyclic_generators g)
[cyclic_generators_gen_cofactor_eq_orders] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀n. n divides CARD G ⇒
cyclic_generators (gen (cyclic_gen g ** (CARD G DIV n))) =
orders g n
[cyclic_generators_nonempty] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒ cyclic_generators g ≠ ∅
[cyclic_generators_subset] Theorem
⊢ ∀g. cyclic_generators g ⊆ G
[cyclic_group] Theorem
⊢ ∀g. cyclic g ⇒ Group g
[cyclic_group_abelian] Theorem
⊢ ∀g. cyclic g ⇒ AbelianGroup g
[cyclic_group_comm] Theorem
⊢ ∀g. cyclic g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x
[cyclic_image_ord_is_divisors] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒ IMAGE ord G = divisors (CARD G)
[cyclic_index_exists] Theorem
⊢ ∀g x.
cyclic g ∧ x ∈ G ⇒
∃n. x = cyclic_gen g ** n ∧ (FINITE G ⇒ n < CARD G)
[cyclic_iso_gen] Theorem
⊢ ∀g h f.
cyclic g ∧ cyclic h ∧ FINITE G ∧ GroupIso f g h ⇒
f (cyclic_gen g) ∈ cyclic_generators h
[cyclic_orders_card] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀n. CARD (orders g n) = if n divides CARD G then phi n else 0
[cyclic_orders_nonempty] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒ ∀n. n divides CARD G ⇒ orders g n ≠ ∅
[cyclic_orders_partition] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G))
[cyclic_subgroup_condition] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀n. (∃h. h ≤ g ∧ CARD H = n) ⇔ n divides CARD G
[cyclic_subgroup_cyclic] Theorem
⊢ ∀g h. cyclic g ∧ h ≤ g ⇒ cyclic h
[cyclic_uroots_cyclic] Theorem
⊢ ∀g. cyclic g ⇒ ∀n. cyclic (uroots n)
[cyclic_uroots_has_primitive] Theorem
⊢ ∀g. FINITE G ∧ cyclic g ⇒
∀n. ∃z.
z ∈ (uroots n).carrier ∧ ord z = CARD (uroots n).carrier
[element_coset_property] Theorem
⊢ ∀g X a. a ∈ G ⇒ ∀x. x ∈ X ⇒ a * x ∈ a * X
[eq_order_equiv] Theorem
⊢ ∀g. eq_order g equiv_on G
[eq_order_is_feq_order] Theorem
⊢ ∀g. eq_order g = feq ord
[fermat_little] Theorem
⊢ ∀p a. prime p ∧ 0 < a ∧ a < p ⇒ a ** (p − 1) MOD p = 1
[fermat_little_alt] Theorem
⊢ ∀p a. prime p ⇒ a ** (p − 1) MOD p = if a MOD p = 0 then 0 else 1
[fermat_little_thm] Theorem
⊢ ∀p. prime p ⇒ ∀a. a ** p MOD p = a MOD p
[fermat_roots] Theorem
⊢ ∀p. prime p ⇒
∀x y z. x ** p + y ** p = z ** p ⇒ (x + y) MOD p = z MOD p
[finite_abelian_Fermat] Theorem
⊢ ∀g a. FiniteAbelianGroup g ∧ a ∈ G ⇒ a ** CARD G = #e
[finite_abelian_group_is_finite_abelian_monoid] Theorem
⊢ ∀g. FiniteAbelianGroup g ⇒ FiniteAbelianMonoid g
[finite_cyclic_group_add_mod_bij] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
BIJ (λn. cyclic_gen g ** n) (add_mod (CARD G)).carrier G
[finite_cyclic_group_add_mod_homo] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
GroupHomo (λn. cyclic_gen g ** n) (add_mod (CARD G)) g
[finite_cyclic_group_add_mod_iso] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
GroupIso (λn. cyclic_gen g ** n) (add_mod (CARD G)) g
[finite_cyclic_group_bij] Theorem
⊢ ∀g1 g2.
cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
CARD g1.carrier = CARD g2.carrier ⇒
BIJ (λx. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier
g2.carrier
[finite_cyclic_group_existence] Theorem
⊢ ∀n. 0 < n ⇒ ∃g. cyclic g ∧ CARD g.carrier = n
[finite_cyclic_group_homo] Theorem
⊢ ∀g1 g2.
cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
CARD g1.carrier = CARD g2.carrier ⇒
GroupHomo (λx. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2
[finite_cyclic_group_iso] Theorem
⊢ ∀g1 g2.
cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
CARD g1.carrier = CARD g2.carrier ⇒
GroupIso (λx. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2
[finite_cyclic_group_uniqueness] Theorem
⊢ ∀g1 g2.
cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
CARD g1.carrier = CARD g2.carrier ⇒
∃f. GroupIso f g1 g2
[finite_cyclic_index_add] Theorem
⊢ ∀g x y.
cyclic g ∧ FINITE G ∧ x ∈ G ∧ y ∈ G ⇒
cyclic_index g (x * y) =
(cyclic_index g x + cyclic_index g y) MOD CARD G
[finite_cyclic_index_property] Theorem
⊢ ∀g. cyclic g ∧ FINITE G ⇒
∀n. n < CARD G ⇒ cyclic_index g (cyclic_gen g ** n) = n
[finite_cyclic_index_unique] Theorem
⊢ ∀g x.
cyclic g ∧ FINITE G ∧ x ∈ G ⇒
∀n. n < CARD G ⇒ (x = cyclic_gen g ** n ⇔ n = cyclic_index g x)
[finite_group_Fermat] Theorem
⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ a ** CARD G = #e
[finite_group_card_pos] Theorem
⊢ ∀g. FiniteGroup g ⇒ 0 < CARD G
[finite_group_exp_not_distinct] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ∃h k. x ** h = x ** k ∧ h ≠ k
[finite_group_exp_period_exists] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ∃k. 0 < k ∧ x ** k = #e
[finite_group_is_finite_monoid] Theorem
⊢ ∀g. FiniteGroup g ⇒ FiniteMonoid g
[finite_group_is_group] Theorem
⊢ ∀g. FiniteGroup g ⇒ Group g
[finite_group_is_monoid] Theorem
⊢ ∀g. FiniteGroup g ⇒ Monoid g
[finite_group_order] Theorem
⊢ ∀g. FiniteGroup g ⇒
∀x. x ∈ G ⇒
∀n. ord x = n ⇒
0 < n ∧ x ** n = #e ∧ ∀m. 0 < m ∧ m < n ⇒ x ** m ≠ #e
[finite_group_primitive_property] Theorem
⊢ ∀g. FiniteGroup g ⇒
∀z. z ∈ G ∧ ord z = CARD G ⇒
∀x. x ∈ G ⇒ ∃n. n < CARD G ∧ x = z ** n
[finite_homo_image] Theorem
⊢ ∀f g1 g2 h.
FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
FINITE
(homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier
[finite_monoid_invertibles_is_finite_group] Theorem
⊢ ∀g. FiniteMonoid g ⇒ FiniteGroup (Invertibles g)
[finite_subgroup_carrier_finite] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀h. h ≤ g ⇒ FINITE H
[finite_subgroup_finite_group] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀h. h ≤ g ⇒ FiniteGroup h
[fixed_points_element] Theorem
⊢ ∀f g X x. x ∈ fixed_points f g X ⇔ x ∈ X ∧ ∀a. a ∈ G ⇒ f a x = x
[fixed_points_element_element] Theorem
⊢ ∀f g X x. x ∈ fixed_points f g X ⇒ x ∈ X
[fixed_points_finite] Theorem
⊢ ∀f g X. FINITE X ⇒ FINITE (fixed_points f g X)
[fixed_points_orbit_iff_sing] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
∀x. x ∈ X ⇒ (x ∈ fixed_points f g X ⇔ SING (orbit f g x))
[fixed_points_orbit_sing] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
∀x. x ∈ fixed_points f g X ⇔ x ∈ X ∧ orbit f g x = {x}
[fixed_points_subset] Theorem
⊢ ∀f g X. fixed_points f g X ⊆ X
[fn_cyclic_group_alt] Theorem
⊢ ∀e f n.
(∃k. k ≠ 0 ∧ FUNPOW f k e = e) ∧
n = (LEAST k. k ≠ 0 ∧ FUNPOW f k e = e) ⇒
(fn_cyclic_group e f).carrier = {FUNPOW f k e | k < n} ∧
(fn_cyclic_group e f).id = e ∧
∀i j.
(fn_cyclic_group e f).op (FUNPOW f i e) (FUNPOW f j e) =
FUNPOW f ((i + j) MOD n) e
[fn_cyclic_group_carrier] Theorem
⊢ ∀e f. (fn_cyclic_group e f).carrier = {x | ∃n. FUNPOW f n e = x}
[fn_cyclic_group_finite_abelian_group] Theorem
⊢ ∀e f.
(∃n. n ≠ 0 ∧ FUNPOW f n e = e) ⇒
FiniteAbelianGroup (fn_cyclic_group e f)
[fn_cyclic_group_finite_group] Theorem
⊢ ∀e f.
(∃n. n ≠ 0 ∧ FUNPOW f n e = e) ⇒
FiniteGroup (fn_cyclic_group e f)
[fn_cyclic_group_group] Theorem
⊢ ∀e f. (∃n. n ≠ 0 ∧ FUNPOW f n e = e) ⇒ Group (fn_cyclic_group e f)
[fn_cyclic_group_id] Theorem
⊢ ∀e f. (fn_cyclic_group e f).id = e
[generated_Fermat] Theorem
⊢ ∀g a.
FiniteGroup g ∧ a ∈ G ⇒ ∀x. x ∈ Gen a ⇒ x ** CARD (Gen a) = #e
[generated_carrier] Theorem
⊢ ∀g a. a ∈ G ⇒ Gen a = IMAGE ($** a) 𝕌(:num)
[generated_carrier_as_image] Theorem
⊢ ∀g. Group g ⇒
∀a. a ∈ G ∧ 0 < ord a ⇒
Gen a = IMAGE (λj. a ** j) (count (ord a))
[generated_carrier_has_id] Theorem
⊢ ∀g a. #e ∈ Gen a
[generated_element] Theorem
⊢ ∀g a x. x ∈ Gen a ⇔ ∃n. x = a ** n
[generated_exp] Theorem
⊢ ∀g a z. a ∈ G ∧ z ∈ Gen a ⇒ ∀n. (gen a).exp z n = z ** n
[generated_finite_group] Theorem
⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ FiniteGroup (gen a)
[generated_gen_element] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x ∈ Gen x
[generated_group] Theorem
⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ Group (gen a)
[generated_group_card] Theorem
⊢ ∀g a. Group g ∧ a ∈ G ∧ 0 < ord a ⇒ CARD (Gen a) = ord a
[generated_group_finite] Theorem
⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ FINITE (Gen a)
[generated_id_carrier] Theorem
⊢ ∀g. Group g ⇒ Gen #e = {#e}
[generated_id_subgroup] Theorem
⊢ ∀g. Group g ⇒ gen #e ≤ g
[generated_image_subset_all_subgroups] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀s. s ⊆ G ⇒ IMAGE gen s ⊆ all_subgroups g
[generated_image_subset_power_set] Theorem
⊢ ∀g. Group g ⇒ ∀s. s ⊆ G ⇒ IMAGE (λa. Gen a) s ⊆ POW G
[generated_property] Theorem
⊢ ∀g a. (gen a).op = $* ∧ (gen a).id = #e
[generated_subgroup] Theorem
⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ gen a ≤ g
[generated_subset] Theorem
⊢ ∀g a. Group g ∧ a ∈ G ⇒ Gen a ⊆ G
[group_all_invertible] Theorem
⊢ ∀g. Group g ⇒ G* = G
[group_alt] Theorem
⊢ ∀g. Group g ⇔
(∀x y::G. x * y ∈ G) ∧ (∀x y z::G. x * y * z = x * (y * z)) ∧
#e ∈ G ∧ (∀x::G. #e * x = x) ∧ ∀x::G. |/ x ∈ G ∧ |/ x * x = #e
[group_assoc] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * y * z = x * (y * z)
[group_auto_I] Theorem
⊢ ∀g. GroupAuto I g
[group_auto_bij] Theorem
⊢ ∀g f. GroupAuto f g ⇒ f PERMUTES G
[group_auto_compose] Theorem
⊢ ∀g f1 f2. GroupAuto f1 g ∧ GroupAuto f2 g ⇒ GroupAuto (f1 ∘ f2) g
[group_auto_element] Theorem
⊢ ∀f g. GroupAuto f g ⇒ ∀x. x ∈ G ⇒ f x ∈ G
[group_auto_exp] Theorem
⊢ ∀g f.
Group g ∧ GroupAuto f g ⇒ ∀x. x ∈ G ⇒ ∀n. f (x ** n) = f x ** n
[group_auto_id] Theorem
⊢ ∀f g. Group g ∧ GroupAuto f g ⇒ f #e = #e
[group_auto_is_monoid_auto] Theorem
⊢ ∀g f. Group g ∧ GroupAuto f g ⇒ MonoidAuto f g
[group_auto_linv_auto] Theorem
⊢ ∀g f. Group g ∧ GroupAuto f g ⇒ GroupAuto (LINV f G) g
[group_auto_order] Theorem
⊢ ∀g f. Group g ∧ GroupAuto f g ⇒ ∀x. x ∈ G ⇒ ord (f x) = ord x
[group_carrier_nonempty] Theorem
⊢ ∀g. Group g ⇒ G ≠ ∅
[group_comm_exp] Theorem
⊢ ∀g. Group g ⇒
∀x y.
x ∈ G ∧ y ∈ G ⇒ x * y = y * x ⇒ ∀n. x ** n * y = y * x ** n
[group_comm_exp_exp] Theorem
⊢ ∀g. Group g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
∀n m. x ** n * y ** m = y ** m * x ** n
[group_comm_op_exp] Theorem
⊢ ∀g. Group g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
∀n. (x * y) ** n = x ** n * y ** n
[group_coset_eq_itself] Theorem
⊢ ∀g a. Group g ∧ a ∈ G ⇒ a * G = G
[group_coset_is_permutation] Theorem
⊢ ∀g a. Group g ∧ a ∈ G ⇒ a * G = G
[group_def_alt] Theorem
⊢ ∀g. Group g ⇔
(∀x y. x ∈ G ∧ y ∈ G ⇒ x * y ∈ G) ∧
(∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * y * z = x * (y * z)) ∧
#e ∈ G ∧ (∀x. x ∈ G ⇒ #e * x = x) ∧
∀x. x ∈ G ⇒ ∃y. y ∈ G ∧ y * x = #e
[group_def_by_inverse] Theorem
⊢ ∀g. Group g ⇔ Monoid g ∧ ∀x. x ∈ G ⇒ ∃y. y ∈ G ∧ y * x = #e
[group_div_cancel] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x / x = #e
[group_div_element] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ x / y ∈ G
[group_div_lsame] Theorem
⊢ ∀g. Group g ⇒
∀x y z.
x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ z * x / (z * y) = z * (x / y) / z
[group_div_pair] Theorem
⊢ ∀g. Group g ⇒
∀x1 y1 x2 y2.
x1 ∈ G ∧ y1 ∈ G ∧ x2 ∈ G ∧ y2 ∈ G ⇒
x1 * y1 / (x2 * y2) = x1 * (y1 / y2) / x1 * (x1 / x2)
[group_div_rsame] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * z / (y * z) = x / y
[group_excluding_exp] Theorem
⊢ ∀g z x n. (g excluding z).exp x n = x ** n
[group_excluding_op] Theorem
⊢ ∀g z. (g excluding z).op = $*
[group_excluding_property] Theorem
⊢ ∀g z.
(g excluding z).op = $* ∧ (g excluding z).id = #e ∧
∀x. x ∈ (g excluding z).carrier ⇒ x ∈ G ∧ x ≠ z
[group_exp_0] Theorem
⊢ ∀g x. x ** 0 = #e
[group_exp_1] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x ** 1 = x
[group_exp_SUC] Theorem
⊢ ∀g x n. x ** SUC n = x * x ** n
[group_exp_add] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n k. x ** (n + k) = x ** n * x ** k
[group_exp_comm] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** n * x = x * x ** n
[group_exp_element] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** n ∈ G
[group_exp_eq] Theorem
⊢ ∀g. Group g ⇒
∀x. x ∈ G ⇒ ∀m n. m < n ∧ x ** m = x ** n ⇒ x ** (n − m) = #e
[group_exp_eq_condition] Theorem
⊢ ∀g x.
Group g ∧ x ∈ G ∧ 0 < ord x ⇒
∀n m. x ** n = x ** m ⇔ n MOD ord x = m MOD ord x
[group_exp_equal] Theorem
⊢ ∀g x.
Group g ∧ x ∈ G ⇒
∀n m. n < ord x ∧ m < ord x ∧ x ** n = x ** m ⇒ n = m
[group_exp_inv] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. |/ (x ** n) = |/ x ** n
[group_exp_mod] Theorem
⊢ ∀g. Group g ⇒
∀x. x ∈ G ∧ 0 < ord x ⇒ ∀n. x ** n = x ** (n MOD ord x)
[group_exp_mod_order] Theorem
⊢ ∀g. Group g ⇒
∀x. x ∈ G ∧ 0 < ord x ⇒ ∀n. x ** n = x ** (n MOD ord x)
[group_exp_mult] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n k. x ** (n * k) = (x ** n) ** k
[group_exp_mult_comm] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀m n. (x ** m) ** n = (x ** n) ** m
[group_exp_suc] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** SUC n = x ** n * x
[group_first_isomorphism_thm] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒
kernel_group f g h << g ∧ homo_image f g h ≤ h ∧
GroupIso (λz. CHOICE (preimage f G z) * kernel f g h)
(homo_image f g h) (g / kernel_group f g h) ∧
(SURJ f G h.carrier ⇒ GroupIso I h (homo_image f g h))
[group_homo_I_refl] Theorem
⊢ ∀g. GroupHomo I g g
[group_homo_compose] Theorem
⊢ ∀g h k f1 f2.
GroupHomo f1 g h ∧ GroupHomo f2 h k ⇒ GroupHomo (f2 ∘ f1) g k
[group_homo_cong] Theorem
⊢ ∀g h f1 f2.
Group g ∧ Group h ∧ (∀x. x ∈ G ⇒ f1 x = f2 x) ⇒
(GroupHomo f1 g h ⇔ GroupHomo f2 g h)
[group_homo_element] Theorem
⊢ ∀f g h. GroupHomo f g h ⇒ ∀x. x ∈ G ⇒ f x ∈ h.carrier
[group_homo_exp] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒
∀x. x ∈ G ⇒ ∀n. f (x ** n) = h.exp (f x) n
[group_homo_homo_image_group] Theorem
⊢ ∀g h f. Group g ∧ MonoidHomo f g h ⇒ Group (homo_image f g h)
[group_homo_id] Theorem
⊢ ∀f g h. Group g ∧ Group h ∧ GroupHomo f g h ⇒ f #e = h.id
[group_homo_image_surj_property] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ SURJ f G h.carrier ⇒
GroupIso I h (homo_image f g h)
[group_homo_inv] Theorem
⊢ ∀f g h.
Group g ∧ Group h ∧ GroupHomo f g h ⇒
∀x. x ∈ G ⇒ f ( |/ x) = h.inv (f x)
[group_homo_is_monoid_homo] Theorem
⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ MonoidHomo f g h
[group_homo_monoid_homo] Theorem
⊢ ∀f g h. GroupHomo f g h ∧ f #e = h.id ⇔ MonoidHomo f g h
[group_homo_sym] Theorem
⊢ ∀g h f.
Group g ∧ GroupHomo f g h ∧ BIJ f G h.carrier ⇒
GroupHomo (LINV f G) h g
[group_homo_sym_any] Theorem
⊢ Group g ∧ GroupHomo f g h ∧
(∀x. x ∈ h.carrier ⇒ i x ∈ G ∧ f (i x) = x) ∧
(∀x. x ∈ G ⇒ i (f x) = x) ⇒
GroupHomo i h g
[group_homo_trans] Theorem
⊢ ∀g h k f1 f2.
GroupHomo f1 g h ∧ GroupHomo f2 h k ⇒ GroupHomo (f2 ∘ f1) g k
[group_id] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ #e * x = x ∧ x * #e = x
[group_id_element] Theorem
⊢ ∀g. Group g ⇒ #e ∈ G
[group_id_exp] Theorem
⊢ ∀g. Group g ⇒ ∀n. #e ** n = #e
[group_id_fix] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ (x * x = x ⇔ x = #e)
[group_id_id] Theorem
⊢ ∀g. Group g ⇒ #e * #e = #e
[group_id_unique] Theorem
⊢ ∀g. Group g ⇒
∀x y.
x ∈ G ∧ y ∈ G ⇒ (y * x = x ⇔ y = #e) ∧ (x * y = x ⇔ y = #e)
[group_image_as_op_image] Theorem
⊢ ∀g. GPI = OP_IMAGE $* #e
[group_image_empty] Theorem
⊢ ∀g f. GPI f ∅ = #e
[group_image_sing] Theorem
⊢ ∀g. Monoid g ⇒ ∀f. gfun f ⇒ ∀x. x ∈ G ⇒ GPI f {x} = f x
[group_including_excluding_abelian] Theorem
⊢ ∀g z.
z ∉ G ⇒
(AbelianGroup g ⇔ AbelianGroup (g including z excluding z))
[group_including_excluding_eqn] Theorem
⊢ ∀g z.
g including z excluding z =
if z ∈ G then <|carrier := G DELETE z; op := $*; id := #e|>
else g
[group_including_excluding_group] Theorem
⊢ ∀g z. z ∉ G ⇒ (Group g ⇔ Group (g including z excluding z))
[group_including_excluding_property] Theorem
⊢ ∀g z.
(g including z excluding z).op = $* ∧
(g including z excluding z).id = #e ∧
(z ∉ G ⇒ (g including z excluding z).carrier = G)
[group_including_property] Theorem
⊢ ∀g z.
(g including z).op = $* ∧ (g including z).id = #e ∧
∀x. x ∈ (g including z).carrier ⇒ x ∈ G ∨ x = z
[group_inj_image_abelian_group] Theorem
⊢ ∀g f.
AbelianGroup g ∧ INJ f G 𝕌(:β) ⇒
AbelianGroup (monoid_inj_image g f)
[group_inj_image_excluding_abelian_group] Theorem
⊢ ∀g f e.
AbelianGroup (g excluding e) ∧ INJ f G 𝕌(:β) ∧ e ∈ G ⇒
AbelianGroup (monoid_inj_image g f excluding f e)
[group_inj_image_excluding_group] Theorem
⊢ ∀g f e.
Group (g excluding e) ∧ INJ f G 𝕌(:β) ∧ e ∈ G ⇒
Group (monoid_inj_image g f excluding f e)
[group_inj_image_group] Theorem
⊢ ∀g f. Group g ∧ INJ f G 𝕌(:β) ⇒ Group (monoid_inj_image g f)
[group_inj_image_group_homo] Theorem
⊢ ∀g f. INJ f G 𝕌(:β) ⇒ GroupHomo f g (monoid_inj_image g f)
[group_inv_element] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ |/ x ∈ G
[group_inv_eq] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ ( |/ x = |/ y ⇔ x = y)
[group_inv_eq_id] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ( |/ x = #e ⇔ x = #e)
[group_inv_eq_swap] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ ( |/ x = y ⇔ x = |/ y)
[group_inv_exp] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. |/ x ** n = |/ (x ** n)
[group_inv_id] Theorem
⊢ ∀g. Group g ⇒ |/ #e = #e
[group_inv_inv] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ |/ ( |/ x) = x
[group_inv_op] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ |/ (x * y) = |/ y * |/ x
[group_inv_order] Theorem
⊢ ∀g x. Group g ∧ x ∈ G ⇒ ord ( |/ x) = ord x
[group_inv_thm] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x * |/ x = #e ∧ |/ x * x = #e
[group_is_monoid] Theorem
⊢ ∀g. Group g ⇒ Monoid g
[group_iso_I_refl] Theorem
⊢ ∀g. GroupIso I g g
[group_iso_bij] Theorem
⊢ ∀g h f. GroupIso f g h ⇒ BIJ f G h.carrier
[group_iso_card_eq] Theorem
⊢ ∀g h f. GroupIso f g h ∧ FINITE G ⇒ CARD G = CARD h.carrier
[group_iso_compose] Theorem
⊢ ∀g h k f1 f2.
GroupIso f1 g h ∧ GroupIso f2 h k ⇒ GroupIso (f2 ∘ f1) g k
[group_iso_element] Theorem
⊢ ∀f g h. GroupIso f g h ⇒ ∀x. x ∈ G ⇒ f x ∈ h.carrier
[group_iso_exp] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupIso f g h ⇒
∀x. x ∈ G ⇒ ∀n. f (x ** n) = h.exp (f x) n
[group_iso_group] Theorem
⊢ ∀g h f. Group g ∧ GroupIso f g h ∧ f #e = h.id ⇒ Group h
[group_iso_id] Theorem
⊢ ∀f g h. Group g ∧ Group h ∧ GroupIso f g h ⇒ f #e = h.id
[group_iso_is_monoid_iso] Theorem
⊢ ∀g h f. Group g ∧ Group h ∧ GroupIso f g h ⇒ MonoidIso f g h
[group_iso_linv_iso] Theorem
⊢ ∀g h f. Group g ∧ GroupIso f g h ⇒ GroupIso (LINV f G) h g
[group_iso_monoid_iso] Theorem
⊢ ∀f g h. GroupIso f g h ∧ f #e = h.id ⇔ MonoidIso f g h
[group_iso_order] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupIso f g h ⇒
∀x. x ∈ G ⇒ order h (f x) = ord x
[group_iso_property] Theorem
⊢ ∀f g h.
GroupIso f g h ⇔
GroupHomo f g h ∧ ∀y. y ∈ h.carrier ⇒ ∃!x. x ∈ G ∧ f x = y
[group_iso_sym] Theorem
⊢ ∀g h f. Group g ∧ GroupIso f g h ⇒ GroupIso (LINV f G) h g
[group_iso_trans] Theorem
⊢ ∀g h k f1 f2.
GroupIso f1 g h ∧ GroupIso f2 h k ⇒ GroupIso (f2 ∘ f1) g k
[group_lcancel] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * y = x * z ⇔ y = z)
[group_lid] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ #e * x = x
[group_lid_unique] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (y * x = x ⇔ y = #e)
[group_linv] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ |/ x * x = #e
[group_linv_assoc] Theorem
⊢ ∀g. Group g ⇒
∀x y. x ∈ G ∧ y ∈ G ⇒ y = x * ( |/ x * y) ∧ y = |/ x * (x * y)
[group_linv_unique] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * y = #e ⇔ x = |/ y)
[group_lsolve] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * y = z ⇔ x = z * |/ y)
[group_normal_equiv] Theorem
⊢ ∀g h. h << g ⇒ $== equiv_on G
[group_normal_equiv_property] Theorem
⊢ ∀h g. h << g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x == y ⇔ x ∈ y * H)
[group_normal_equiv_reflexive] Theorem
⊢ ∀g h. h << g ⇒ ∀z. z ∈ G ⇒ z == z
[group_normal_equiv_symmetric] Theorem
⊢ ∀g h. h << g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x == y ⇔ y == x)
[group_normal_equiv_transitive] Theorem
⊢ ∀g h.
h << g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x == y ∧ y == z ⇒ x == z
[group_op_element] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y ∈ G
[group_op_linv_eq_id] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ ( |/ x * y = #e ⇔ x = y)
[group_op_linv_eqn] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ ( |/ x * y = z ⇔ y = x * z)
[group_op_rinv_eq_id] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * |/ y = #e ⇔ x = y)
[group_op_rinv_eqn] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * |/ y = z ⇔ x = z * y)
[group_order_cofactor] Theorem
⊢ ∀g. Group g ⇒
∀x n.
x ∈ G ∧ 0 < ord x ∧ n divides ord x ⇒
ord (x ** (ord x DIV n)) = n
[group_order_common] Theorem
⊢ ∀g. Group g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
∃z. z ∈ G ∧ ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y)
[group_order_common_coprime] Theorem
⊢ ∀g. Group g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ∧ coprime (ord x) (ord y) ⇒
∃z. z ∈ G ∧ ord z = ord x * ord y
[group_order_condition] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀m. x ** m = #e ⇔ ord x divides m
[group_order_divides] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ord x divides CARD G
[group_order_divides_exp] Theorem
⊢ ∀g x. Group g ∧ x ∈ G ⇒ ∀n. x ** n = #e ⇔ ord x divides n
[group_order_divides_maximal] Theorem
⊢ ∀g. FiniteAbelianGroup g ⇒
∀x. x ∈ G ⇒ ord x divides maximal_order g
[group_order_divisor] Theorem
⊢ ∀g. Group g ⇒
∀x m.
x ∈ G ∧ 0 < ord x ∧ m divides ord x ⇒ ∃y. y ∈ G ∧ ord y = m
[group_order_eq_1] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ (ord x = 1 ⇔ x = #e)
[group_order_exp_cofactor] Theorem
⊢ ∀g x n.
Group g ∧ x ∈ G ∧ 0 < ord x ∧ n divides ord x ⇒
ord (x ** (ord x DIV n)) = n
[group_order_id] Theorem
⊢ ∀g. Group g ⇒ ord #e = 1
[group_order_inv] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ∧ 0 < ord x ⇒ |/ x = x ** (ord x − 1)
[group_order_nonzero] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ord x ≠ 0
[group_order_pos] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ 0 < ord x
[group_order_power] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀k. ord (x ** k) * gcd (ord x) k = ord x
[group_order_power_coprime] Theorem
⊢ ∀g. Group g ⇒
∀x. x ∈ G ⇒ ∀n. coprime n (ord x) ⇒ ord (x ** n) = ord x
[group_order_power_eq_0] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀k. ord (x ** k) = 0 ⇔ 0 < k ∧ ord x = 0
[group_order_power_eq_order] Theorem
⊢ ∀g x.
Group g ∧ x ∈ G ∧ 0 < ord x ⇒
∀k. ord (x ** k) = ord x ⇔ coprime k (ord x)
[group_order_power_eqn] Theorem
⊢ ∀g. Group g ⇒
∀x k. x ∈ G ∧ 0 < k ⇒ ord (x ** k) = ord x DIV gcd k (ord x)
[group_order_property] Theorem
⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ 0 < ord x ∧ x ** ord x = #e
[group_order_thm] Theorem
⊢ ∀g n.
0 < n ⇒
∀x. ord x = n ⇔ x ** n = #e ∧ ∀m. 0 < m ∧ m < n ⇒ x ** m ≠ #e
[group_order_to_generated_bij] Theorem
⊢ ∀g a.
Group g ∧ a ∈ G ∧ 0 < ord a ⇒
BIJ (λn. a ** n) (count (ord a)) (Gen a)
[group_order_unique] Theorem
⊢ ∀g. Group g ⇒
∀x. x ∈ G ⇒
∀m n. m < ord x ∧ n < ord x ∧ x ** m = x ** n ⇒ m = n
[group_orders_eq_1] Theorem
⊢ ∀g. Group g ⇒ orders g 1 = {#e}
[group_pair_reduce] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * z * |/ (y * z) = x * |/ y
[group_rcancel] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (y * x = z * x ⇔ y = z)
[group_rid] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x * #e = x
[group_rid_unique] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * y = x ⇔ y = #e)
[group_rinv] Theorem
⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x * |/ x = #e
[group_rinv_assoc] Theorem
⊢ ∀g. Group g ⇒
∀x y. x ∈ G ∧ y ∈ G ⇒ y = y * |/ x * x ∧ y = y * x * |/ x
[group_rinv_unique] Theorem
⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * y = #e ⇔ y = |/ x)
[group_rsolve] Theorem
⊢ ∀g. Group g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * y = z ⇔ y = |/ x * z)
[group_uroots_group] Theorem
⊢ ∀g. AbelianGroup g ⇒ ∀n. Group (uroots n)
[group_uroots_has_id] Theorem
⊢ ∀g. Group g ⇒ ∀n. #e ∈ (uroots n).carrier
[group_uroots_subgroup] Theorem
⊢ ∀g. AbelianGroup g ⇒ ∀n. uroots n ≤ g
[homo_count_formula] Theorem
⊢ ∀f g1 g2 h.
FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
CARD (preimage_group f g1 g2 h.carrier).carrier =
CARD
(kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier *
CARD
(preimage_group f g1 g2 h.carrier /
kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier
[homo_group_abelian_group] Theorem
⊢ ∀g f.
AbelianGroup g ∧ GroupHomo f g (homo_group g f) ⇒
AbelianGroup (homo_group g f)
[homo_group_assoc] Theorem
⊢ ∀g f.
Group g ∧ GroupHomo f g (homo_group g f) ⇒
∀x y z. x ∈ fG ∧ y ∈ fG ∧ z ∈ fG ⇒ (x ∘ y) ∘ z = x ∘ y ∘ z
[homo_group_by_inj] Theorem
⊢ ∀g f. Group g ∧ INJ f G 𝕌(:β) ⇒ GroupHomo f g (homo_group g f)
[homo_group_closure] Theorem
⊢ ∀g f.
Group g ∧ GroupHomo f g (homo_group g f) ⇒
∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y ∈ fG
[homo_group_comm] Theorem
⊢ ∀g f.
AbelianGroup g ∧ GroupHomo f g (homo_group g f) ⇒
∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y = y ∘ x
[homo_group_group] Theorem
⊢ ∀g f.
Group g ∧ GroupHomo f g (homo_group g f) ⇒ Group (homo_group g f)
[homo_group_id] Theorem
⊢ ∀g f.
Group g ∧ GroupHomo f g (homo_group g f) ⇒
#i ∈ fG ∧ ∀x. x ∈ fG ⇒ #i ∘ x = x ∧ x ∘ #i = x
[homo_group_inv] Theorem
⊢ ∀g f.
Group g ∧ GroupHomo f g (homo_group g f) ⇒
∀x. x ∈ fG ⇒ ∃z. z ∈ fG ∧ z ∘ x = #i
[homo_image_group] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒ Group (homo_image f g h)
[homo_image_homo_quotient_kernel] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒
GroupHomo (λz. CHOICE (preimage f G z) * kernel f g h)
(homo_image f g h) (g / kernel_group f g h)
[homo_image_iso_quotient_kernel] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒
GroupIso (λz. CHOICE (preimage f G z) * kernel f g h)
(homo_image f g h) (g / kernel_group f g h)
[homo_image_monoid] Theorem
⊢ ∀g h f.
Monoid g ∧ Monoid h ∧ MonoidHomo f g h ⇒
Monoid (homo_image f g h)
[homo_image_subgroup] Theorem
⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ homo_image f g h ≤ h
[homo_image_to_quotient_kernel_bij] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒
BIJ (λz. CHOICE (preimage f G z) * kernel f g h)
(homo_image f g h).carrier (g / kernel_group f g h).carrier
[homo_restrict_same_kernel] Theorem
⊢ ∀f g1 g2 h.
H ⊆ g1.carrier ∧ GroupHomo f g1 g2 ∧ kernel f g1 g2 ⊆ H ⇒
kernel f g1 g2 = kernel f h g2
[image_iso_preimage_quotient] Theorem
⊢ ∀f g1 g2 h.
Group g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
GroupIso
(λz.
coset (preimage_group f g1 g2 h.carrier)
(CHOICE
(preimage f
(preimage_group f g1 g2 h.carrier).carrier z))
(kernel f (preimage_group f g1 g2 h.carrier) g2))
(homo_image f (preimage_group f g1 g2 h.carrier) g2)
(preimage_group f g1 g2 h.carrier /
kernel_group f (preimage_group f g1 g2 h.carrier) g2)
[image_preimage_group] Theorem
⊢ ∀f g1 g2 h.
Group g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ∧
SURJ f g1.carrier g2.carrier ⇒
IMAGE f (PREIMAGE f h.carrier ∩ g1.carrier) = h.carrier
[image_preimage_quotient_same_card] Theorem
⊢ ∀f g1 g2 h.
FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
CARD (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier =
CARD
(preimage_group f g1 g2 h.carrier /
kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier
[image_subgroup_subgroup] Theorem
⊢ ∀g1 g2 h f.
Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧ h ≤ g1 ⇒
homo_image f h g2 ≤ g2
[inCoset_equiv_on_carrier] Theorem
⊢ ∀g h. h ≤ g ⇒ inCoset g h equiv_on G
[inCoset_refl] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀a. a ∈ G ⇒ inCoset g h a a
[inCoset_sym] Theorem
⊢ ∀g h.
h ≤ g ⇒ ∀a b. a ∈ G ∧ b ∈ G ∧ inCoset g h a b ⇒ inCoset g h b a
[inCoset_trans] Theorem
⊢ ∀g h.
h ≤ g ⇒
∀a b c.
a ∈ G ∧ b ∈ G ∧ c ∈ G ∧ inCoset g h a b ∧ inCoset g h b c ⇒
inCoset g h a c
[in_coset] Theorem
⊢ ∀g X a. a ∈ G ⇒ ∀x. x ∈ a * X ⇔ ∃y. y ∈ X ∧ x = a * y
[independent_generated_eq] Theorem
⊢ ∀g. Group g ⇒
∀a b.
a ∈ G ∧ b ∈ G ∧ independent g a b ⇒ (gen a = gen b ⇔ a = b)
[independent_generator_2_card] Theorem
⊢ ∀g. FiniteGroup g ⇒
∀a b.
a ∈ G ∧ b ∈ G ∧ independent g a b ⇒
CARD (gen a ∘ gen b).carrier = ord a * ord b
[independent_sym] Theorem
⊢ ∀g a b. independent g a b ⇔ independent g b a
[iso_group_same_card] Theorem
⊢ ∀f g h. FINITE G ∧ GroupIso f g h ⇒ CARD G = CARD h.carrier
[kernel_element] Theorem
⊢ ∀g h f x. x ∈ kernel f g h ⇔ x ∈ G ∧ f x = h.id
[kernel_group_group] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒ Group (kernel_group f g h)
[kernel_group_normal] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒ kernel_group f g h << g
[kernel_group_subgroup] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒ kernel_group f g h ≤ g
[kernel_property] Theorem
⊢ ∀g h f x. x ∈ kernel f g h ⇔ x ∈ G ∧ f x = h.id
[kernel_quotient_group] Theorem
⊢ ∀g h f.
Group g ∧ Group h ∧ GroupHomo f g h ⇒
Group (g / kernel_group f g h)
[left_coset_alt] Theorem
⊢ ∀g X a. left_coset g X a = {a * z | z ∈ X}
[make_group_property] Theorem
⊢ ∀g s.
(make_group g s).carrier = s ∧ (make_group g s).op = $* ∧
(make_group g s).id = #e
[monoid_homo_homo_image_monoid] Theorem
⊢ ∀g h f. Monoid g ∧ MonoidHomo f g h ⇒ Monoid (homo_image f g h)
[monoid_inv_id] Theorem
⊢ ∀g. Monoid g ⇒ |/ #e = #e
[monoid_inv_order] Theorem
⊢ ∀g x. Monoid g ∧ x ∈ G* ⇒ ord ( |/ x) = ord x
[monoid_inv_order_property] Theorem
⊢ ∀g. FiniteMonoid g ⇒ ∀x. x ∈ G* ⇒ 0 < ord x ∧ x ** ord x = #e
[monoid_invertibles_is_group] Theorem
⊢ ∀g. Monoid g ⇒ Group (Invertibles g)
[mult_mod_abelian_group] Theorem
⊢ ∀p. prime p ⇒ AbelianGroup (mult_mod p)
[mult_mod_card] Theorem
⊢ ∀p. 0 < p ⇒ CARD (mult_mod p).carrier = p − 1
[mult_mod_carrier] Theorem
⊢ ∀p. (mult_mod p).carrier = {i | i ≠ 0 ∧ i < p}
[mult_mod_carrier_alt] Theorem
⊢ ∀p. (mult_mod p).carrier = residue p
[mult_mod_element] Theorem
⊢ ∀p x. x ∈ (mult_mod p).carrier ⇔ x ≠ 0 ∧ x < p
[mult_mod_element_alt] Theorem
⊢ ∀p x. x ∈ (mult_mod p).carrier ⇔ 0 < x ∧ x < p
[mult_mod_eval] Theorem
⊢ ∀p. (mult_mod p).carrier = {i | i ≠ 0 ∧ i < p} ∧
(∀x y. (mult_mod p).op x y = (x * y) MOD p) ∧
(mult_mod p).id = 1
[mult_mod_exp] Theorem
⊢ ∀p a.
prime p ∧ a ∈ (mult_mod p).carrier ⇒
∀n. (mult_mod p).exp a n = a ** n MOD p
[mult_mod_finite] Theorem
⊢ ∀p. FINITE (mult_mod p).carrier
[mult_mod_finite_abelian_group] Theorem
⊢ ∀p. prime p ⇒ FiniteAbelianGroup (mult_mod p)
[mult_mod_finite_group] Theorem
⊢ ∀p. prime p ⇒ FiniteGroup (mult_mod p)
[mult_mod_group] Theorem
⊢ ∀p. prime p ⇒ Group (mult_mod p)
[mult_mod_id] Theorem
⊢ ∀p. (mult_mod p).id = 1
[mult_mod_inv] Theorem
⊢ ∀p. prime p ⇒
∀x. 0 < x ∧ x < p ⇒
(mult_mod p).inv x =
(mult_mod p).exp x (order (mult_mod p) x − 1)
[mult_mod_inv_compute] Theorem
⊢ ∀p x.
(mult_mod p).inv x =
if prime p ∧ 0 < x ∧ x < p then
(mult_mod p).exp x (order (mult_mod p) x − 1)
else FAIL ((mult_mod p).inv x) bad_element
[mult_mod_inverse] Theorem
⊢ ∀p. prime p ⇒
∀a. 0 < a ∧ a < p ⇒ (mult_mod p).inv a = a ** (p − 2) MOD p
[mult_mod_inverse_compute] Theorem
⊢ ∀p a.
(mult_mod p).inv a =
if prime p ∧ 0 < a ∧ a < p then a ** (p − 2) MOD p
else (mult_mod p).inv a
[mult_mod_property] Theorem
⊢ ∀p. (∀x. x ∈ (mult_mod p).carrier ⇒ x ≠ 0) ∧
(∀x. x ∈ (mult_mod p).carrier ⇔ 0 < x ∧ x < p) ∧
(mult_mod p).id = 1 ∧
(∀x y. (mult_mod p).op x y = (x * y) MOD p) ∧
FINITE (mult_mod p).carrier ∧
(0 < p ⇒ CARD (mult_mod p).carrier = p − 1)
[multi_orbits_element] Theorem
⊢ ∀f g X e. e ∈ multi_orbits f g X ⇔ e ∈ orbits f g X ∧ ¬SING e
[multi_orbits_element_finite] Theorem
⊢ ∀f g X e.
(g act X) f ∧ FINITE X ∧ e ∈ multi_orbits f g X ⇒ FINITE e
[multi_orbits_element_subset] Theorem
⊢ ∀f g X e. (g act X) f ∧ e ∈ multi_orbits f g X ⇒ e ⊆ X
[multi_orbits_finite] Theorem
⊢ ∀f g X. FINITE X ⇒ FINITE (multi_orbits f g X)
[multi_orbits_subset] Theorem
⊢ ∀f g X. multi_orbits f g X ⊆ orbits f g X
[non_fixed_points_card] Theorem
⊢ ∀f g X.
FINITE X ⇒
CARD (X DIFF fixed_points f g X) =
CARD X − CARD (fixed_points f g X)
[non_fixed_points_orbit_not_sing] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
∀x. x ∈ X DIFF fixed_points f g X ⇔ x ∈ X ∧ ¬SING (orbit f g x)
[normal_cogen_property] Theorem
⊢ ∀g h. h << g ⇒ ∀x. x ∈ G ⇒ x / cogen g h (x * H) ∈ H
[normal_coset_op_property] Theorem
⊢ ∀g h.
h << g ⇒
∀x y.
x ∈ CosetPartition g h ∧ y ∈ CosetPartition g h ⇒
x ∘ y =
CHOICE (preimage (left_coset g H) G x) *
CHOICE (preimage (left_coset g H) G y) * H
[normal_coset_property] Theorem
⊢ ∀g h.
h << g ⇒
∀a b.
a ∈ G ∧ b ∈ G ⇒
cogen g h (a * H) * cogen g h (b * H) * H = a * b * H
[normal_coset_property1] Theorem
⊢ ∀g h.
h << g ⇒
∀a b. a ∈ G ∧ b ∈ G ⇒ cogen g h (a * H) * b * H = a * b * H
[normal_coset_property2] Theorem
⊢ ∀g h.
h << g ⇒
∀a b. a ∈ G ∧ b ∈ G ⇒ a * cogen g h (b * H) * H = a * b * H
[normal_iff_preimage_normal] Theorem
⊢ ∀f g1 g2 h2.
Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ∧
SURJ f g1.carrier g2.carrier ⇒
(h2 << g2 ⇔ preimage_group f g1 g2 h2.carrier << g1)
[normal_preimage_normal] Theorem
⊢ ∀f g1 g2 h2.
Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ⇒
h2 << g2 ⇒
preimage_group f g1 g2 h2.carrier << g1
[normal_subgroup_alt] Theorem
⊢ ∀g h. h << g ⇔ h ≤ g ∧ ∀a. a ∈ G ⇒ a * H = H * a
[normal_subgroup_antisym] Theorem
⊢ ∀g h. h << g ∧ g << h ⇒ h = g
[normal_subgroup_coset_eq] Theorem
⊢ ∀g h. h << g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * H = y * H ⇔ x / y ∈ H)
[normal_subgroup_coset_homo] Theorem
⊢ ∀g h. h << g ⇒ GroupHomo (left_coset g H) g (g / h)
[normal_subgroup_groups] Theorem
⊢ ∀g h. h << g ⇒ h ≤ g ∧ Group h ∧ Group g
[normal_subgroup_property] Theorem
⊢ ∀h g. h << g ⇒ ∀a z. a ∈ G ∧ z ∈ H ⇒ a * z / a ∈ H
[normal_subgroup_refl] Theorem
⊢ ∀g. Group g ⇒ g << g
[normal_subgroup_subgroup] Theorem
⊢ ∀h g. h << g ⇒ h ≤ g
[normal_surj_normal] Theorem
⊢ ∀f g1 g2 h2.
Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ∧
SURJ f g1.carrier g2.carrier ⇒
preimage_group f g1 g2 h2.carrier << g1 ⇒
h2 << g2
[orbit_alt] Theorem
⊢ ∀f g x. orbit f g x = {f a x | a ∈ G}
[orbit_card_divides_target_card] Theorem
⊢ ∀f g X x.
FiniteGroup g ∧ (g act X) f ∧ x ∈ X ∧ FINITE X ⇒
CARD (orbit f g x) divides CARD G
[orbit_element] Theorem
⊢ ∀f g x y. y ∈ orbit f g x ⇔ (x ~~ y) f g
[orbit_element_in_target] Theorem
⊢ ∀f g X x y. (g act X) f ∧ x ∈ X ∧ y ∈ orbit f g x ⇒ y ∈ X
[orbit_eq_equiv_class] Theorem
⊢ ∀f g X x.
(g act X) f ∧ x ∈ X ⇒ orbit f g x = equiv_class (reach f g) X x
[orbit_eq_orbit] Theorem
⊢ ∀f g X x y.
Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ X ⇒
(orbit f g x = orbit f g y ⇔ (x ~~ y) f g)
[orbit_finite] Theorem
⊢ ∀f g x. FINITE G ⇒ FINITE (orbit f g x)
[orbit_finite_by_target] Theorem
⊢ ∀f g X x. (g act X) f ∧ x ∈ X ∧ FINITE X ⇒ FINITE (orbit f g x)
[orbit_finite_inj_card_eq] Theorem
⊢ ∀f g X x.
(g act X) f ∧ x ∈ X ∧ FINITE X ∧ INJ (λa. f a x) G (orbit f g x) ⇒
CARD (orbit f g x) = CARD G
[orbit_has_action_element] Theorem
⊢ ∀f g x a. a ∈ G ⇒ f a x ∈ orbit f g x
[orbit_has_self] Theorem
⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ x ∈ orbit f g x
[orbit_is_orbits_element] Theorem
⊢ ∀f g X x. x ∈ X ⇒ orbit f g x ∈ orbits f g X
[orbit_sing_fixed_points] Theorem
⊢ ∀f g X.
(g act X) f ⇒
∀x. x ∈ X ∧ orbit f g x = {x} ⇒ x ∈ fixed_points f g X
[orbit_stabilizer_cosets_bij] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒
BIJ (λy. act_by f g x y * stabilizer f g x) (orbit f g x)
{a * stabilizer f g x | a | a ∈ G}
[orbit_stabilizer_cosets_bij_alt] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒
BIJ (λy. act_by f g x y * stabilizer f g x) (orbit f g x)
(CosetPartition g (StabilizerGroup f g x))
[orbit_stabilizer_map_good] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒
∀a b.
a ∈ G ∧ b ∈ G ∧ f a x = f b x ⇒
a * stabilizer f g x = b * stabilizer f g x
[orbit_stabilizer_map_inj] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒
∀a b.
a ∈ G ∧ b ∈ G ∧ a * stabilizer f g x = b * stabilizer f g x ⇒
f a x = f b x
[orbit_stabilizer_thm] Theorem
⊢ ∀f g X x.
FiniteGroup g ∧ (g act X) f ∧ x ∈ X ∧ FINITE X ⇒
CARD G = CARD (orbit f g x) * CARD (stabilizer f g x)
[orbit_subset_target] Theorem
⊢ ∀f g X x. (g act X) f ∧ x ∈ X ⇒ orbit f g x ⊆ X
[orbits_alt] Theorem
⊢ ∀f g X. orbits f g X = {orbit f g x | x ∈ X}
[orbits_element] Theorem
⊢ ∀f g X e. e ∈ orbits f g X ⇔ ∃x. x ∈ X ∧ e = orbit f g x
[orbits_element_element] Theorem
⊢ ∀f g X e x. (g act X) f ∧ e ∈ orbits f g X ∧ x ∈ e ⇒ x ∈ X
[orbits_element_finite] Theorem
⊢ ∀f g X. (g act X) f ∧ FINITE X ⇒ EVERY_FINITE (orbits f g X)
[orbits_element_is_orbit] Theorem
⊢ ∀f g X e x.
Group g ∧ (g act X) f ∧ e ∈ orbits f g X ∧ x ∈ e ⇒
e = orbit f g x
[orbits_element_nonempty] Theorem
⊢ ∀f g X. Group g ∧ (g act X) f ⇒ ∀e. e ∈ orbits f g X ⇒ e ≠ ∅
[orbits_element_subset] Theorem
⊢ ∀f g X e. (g act X) f ∧ e ∈ orbits f g X ⇒ e ⊆ X
[orbits_eq_partition] Theorem
⊢ ∀f g X. (g act X) f ⇒ orbits f g X = partition (reach f g) X
[orbits_equal_size_partition_equal_size] Theorem
⊢ ∀f g X n.
Group g ∧ (g act X) f ∧ FINITE X ∧
(∀x. x ∈ X ⇒ CARD (orbit f g x) = n) ⇒
∀e. e ∈ orbits f g X ⇒ CARD e = n
[orbits_equal_size_property] Theorem
⊢ ∀f g X n.
Group g ∧ (g act X) f ∧ FINITE X ∧
(∀x. x ∈ X ⇒ CARD (orbit f g x) = n) ⇒
n divides CARD X
[orbits_finite] Theorem
⊢ ∀f g X. FINITE X ⇒ FINITE (orbits f g X)
[orbits_size_factor_partition_factor] Theorem
⊢ ∀f g X n.
Group g ∧ (g act X) f ∧ FINITE X ∧
(∀x. x ∈ X ⇒ n divides CARD (orbit f g x)) ⇒
∀e. e ∈ orbits f g X ⇒ n divides CARD e
[orbits_size_factor_property] Theorem
⊢ ∀f g X n.
Group g ∧ (g act X) f ∧ FINITE X ∧
(∀x. x ∈ X ⇒ n divides CARD (orbit f g x)) ⇒
n divides CARD X
[orders_is_feq_class_order] Theorem
⊢ ∀g. orders g = preimage ord G
[preimage_cardinality] Theorem
⊢ ∀f g1 g2 h.
FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ∧
SURJ f g1.carrier g2.carrier ⇒
CARD (preimage_group f g1 g2 h.carrier).carrier =
CARD h.carrier * CARD (kernel f g1 g2)
[preimage_group_group] Theorem
⊢ ∀f g1 g2 h.
Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧ h ≤ g2 ⇒
Group (preimage_group f g1 g2 h.carrier)
[preimage_group_property] Theorem
⊢ ∀f g1 g2 h x.
x ∈ PREIMAGE f h ∩ g1.carrier ⇒ x ∈ g1.carrier ∧ f x ∈ h
[preimage_image_subset] Theorem
⊢ ∀f g1 g2 h.
Group g1 ∧ Group g2 ∧ h ≤ g1 ∧ GroupHomo f g1 g2 ∧
SURJ f g1.carrier g2.carrier ∧ kernel f g1 g2 ⊆ H ⇒
PREIMAGE f (IMAGE f H) ∩ g1.carrier ⊆ H
[preimage_subgroup_kernel] Theorem
⊢ ∀f g1 g2 h2.
Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ⇒
kernel f g1 g2 ⊆ PREIMAGE f h2.carrier ∩ g1.carrier
[preimage_subgroup_subgroup] Theorem
⊢ ∀f g1 g2 h.
Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧ h ≤ g2 ⇒
preimage_group f g1 g2 h.carrier ≤ g1
[prod_image_as_op_image] Theorem
⊢ Π = OP_IMAGE (λx y. x * y) 1
[quotient_group_assoc] Theorem
⊢ ∀g h.
h << g ⇒
∀x y z.
x ∈ CosetPartition g h ∧ y ∈ CosetPartition g h ∧
z ∈ CosetPartition g h ⇒
(x ∘ y) ∘ z = x ∘ y ∘ z
[quotient_group_closure] Theorem
⊢ ∀g h.
h ≤ g ⇒
∀x y.
x ∈ CosetPartition g h ∧ y ∈ CosetPartition g h ⇒
x ∘ y ∈ CosetPartition g h
[quotient_group_group] Theorem
⊢ ∀g h. h << g ⇒ Group (g / h)
[quotient_group_id] Theorem
⊢ ∀g h.
h << g ⇒
H ∈ CosetPartition g h ∧ ∀x. x ∈ CosetPartition g h ⇒ H ∘ x = x
[quotient_group_inv] Theorem
⊢ ∀g h.
h << g ⇒
∀x. x ∈ CosetPartition g h ⇒
∃y. y ∈ CosetPartition g h ∧ y ∘ x = H
[reach_equiv] Theorem
⊢ ∀f g X. Group g ∧ (g act X) f ⇒ reach f g equiv_on X
[reach_refl] Theorem
⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ (x ~~ x) f g
[reach_sym] Theorem
⊢ ∀f g X x y.
Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ X ∧ (x ~~ y) f g ⇒
(y ~~ x) f g
[reach_trans] Theorem
⊢ ∀f g X x y z.
Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X ∧ (x ~~ y) f g ∧
(y ~~ z) f g ⇒
(x ~~ z) f g
[right_coset_alt] Theorem
⊢ ∀g X a. X * a = {z * a | z ∈ X}
[roots_of_unity_0] Theorem
⊢ ∀g. (uroots 0).carrier = G
[roots_of_unity_element] Theorem
⊢ ∀g n x. x ∈ (uroots n).carrier ⇔ x ∈ G ∧ x ** n = #e
[roots_of_unity_subset] Theorem
⊢ ∀g n. (uroots n).carrier ⊆ G
[sing_orbits_card_eqn] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ∧ FINITE X ⇒
CARD (sing_orbits f g X) = CARD (fixed_points f g X)
[sing_orbits_element] Theorem
⊢ ∀f g X e. e ∈ sing_orbits f g X ⇔ e ∈ orbits f g X ∧ SING e
[sing_orbits_element_card] Theorem
⊢ ∀f g X e. e ∈ sing_orbits f g X ⇒ CARD e = 1
[sing_orbits_element_choice] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
∀e. e ∈ sing_orbits f g X ⇒ CHOICE e ∈ fixed_points f g X
[sing_orbits_element_finite] Theorem
⊢ ∀f g X e. e ∈ sing_orbits f g X ⇒ FINITE e
[sing_orbits_element_subset] Theorem
⊢ ∀f g X e. (g act X) f ∧ e ∈ sing_orbits f g X ⇒ e ⊆ X
[sing_orbits_finite] Theorem
⊢ ∀f g X. FINITE X ⇒ FINITE (sing_orbits f g X)
[sing_orbits_subset] Theorem
⊢ ∀f g X. sing_orbits f g X ⊆ orbits f g X
[sing_orbits_to_fixed_points_bij] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
BIJ (λe. CHOICE e) (sing_orbits f g X) (fixed_points f g X)
[sing_orbits_to_fixed_points_inj] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
INJ (λe. CHOICE e) (sing_orbits f g X) (fixed_points f g X)
[sing_orbits_to_fixed_points_surj] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ⇒
SURJ (λe. CHOICE e) (sing_orbits f g X) (fixed_points f g X)
[stabilizer_as_image] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒
stabilizer f g x = IMAGE (λa. if f a x = x then a else #e) G
[stabilizer_conjugate] Theorem
⊢ ∀f g X x a.
Group g ∧ (g act X) f ∧ x ∈ X ∧ a ∈ G ⇒
conjugate g a (stabilizer f g x) = stabilizer f g (f a x)
[stabilizer_element] Theorem
⊢ ∀f g x a. a ∈ stabilizer f g x ⇔ a ∈ G ∧ f a x = x
[stabilizer_group_card_divides] Theorem
⊢ ∀f g X x.
FiniteGroup g ∧ (g act X) f ∧ x ∈ X ⇒
CARD (stabilizer f g x) divides CARD G
[stabilizer_group_carrier] Theorem
⊢ ∀f g x. (StabilizerGroup f g x).carrier = stabilizer f g x
[stabilizer_group_finite_group] Theorem
⊢ ∀f g X x.
FiniteGroup g ∧ (g act X) f ∧ x ∈ X ⇒
FiniteGroup (StabilizerGroup f g x)
[stabilizer_group_group] Theorem
⊢ ∀f g X x.
Group g ∧ (g act X) f ∧ x ∈ X ⇒ Group (StabilizerGroup f g x)
[stabilizer_group_id] Theorem
⊢ ∀f g x. (StabilizerGroup f g x).id = #e
[stabilizer_group_property] Theorem
⊢ ∀f g x.
(StabilizerGroup f g x).carrier = stabilizer f g x ∧
(StabilizerGroup f g x).op = $* ∧ (StabilizerGroup f g x).id = #e
[stabilizer_group_subgroup] Theorem
⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ StabilizerGroup f g x ≤ g
[stabilizer_has_id] Theorem
⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ #e ∈ stabilizer f g x
[stabilizer_nonempty] Theorem
⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ stabilizer f g x ≠ ∅
[stabilizer_subset] Theorem
⊢ ∀f g x. stabilizer f g x ⊆ G
[subgroup_I_antisym] Theorem
⊢ ∀g h. subgroup h g ∧ subgroup g h ⇒ GroupIso I h g
[subgroup_alt] Theorem
⊢ ∀g. Group g ⇒
∀h. h ≤ g ⇔
H ≠ ∅ ∧ H ⊆ G ∧ $o = $* ∧ #i = #e ∧
∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H
[subgroup_antisym] Theorem
⊢ ∀g h. h ≤ g ∧ g ≤ h ⇒ h = g
[subgroup_big_cross_empty] Theorem
⊢ ∀g. sgbcross ∅ = gen #e
[subgroup_big_cross_insert] Theorem
⊢ ∀g. FiniteAbelianGroup g ⇒
∀B. B ⊆ all_subgroups g ⇒
∀h. h ∈ all_subgroups g ∧ h ∉ B ⇒
sgbcross (h INSERT B) = h ∘ sgbcross B
[subgroup_big_cross_thm] Theorem
⊢ ∀g. FiniteAbelianGroup g ⇒
∀B. B ⊆ all_subgroups g ⇒
∀h. h ∈ all_subgroups g ⇒
sgbcross (h INSERT B) = h ∘ sgbcross (B DELETE h)
[subgroup_big_intersect_element] Theorem
⊢ ∀g x. x ∈ (sgbINTER g).carrier ⇔ ∀h. h ≤ g ⇒ x ∈ H
[subgroup_big_intersect_group] Theorem
⊢ ∀g. Group g ⇒ Group (sgbINTER g)
[subgroup_big_intersect_has_id] Theorem
⊢ ∀g. (sgbINTER g).id ∈ (sgbINTER g).carrier
[subgroup_big_intersect_has_inv] Theorem
⊢ ∀g x. x ∈ (sgbINTER g).carrier ⇒ |/ x ∈ (sgbINTER g).carrier
[subgroup_big_intersect_op_element] Theorem
⊢ ∀g x y.
x ∈ (sgbINTER g).carrier ∧ y ∈ (sgbINTER g).carrier ⇒
(sgbINTER g).op x y ∈ (sgbINTER g).carrier
[subgroup_big_intersect_property] Theorem
⊢ ∀g. (sgbINTER g).carrier = BIGINTER (IMAGE (λh. H) {h | h ≤ g}) ∧
(∀x y.
x ∈ (sgbINTER g).carrier ∧ y ∈ (sgbINTER g).carrier ⇒
(sgbINTER g).op x y = x * y) ∧ (sgbINTER g).id = #e
[subgroup_big_intersect_subgroup] Theorem
⊢ ∀g. Group g ⇒ sgbINTER g ≤ g
[subgroup_big_intersect_subset] Theorem
⊢ ∀g. Group g ⇒ (sgbINTER g).carrier ⊆ G
[subgroup_carrier_antisym] Theorem
⊢ ∀g h. subgroup h g ∧ G ⊆ H ⇒ GroupIso I h g
[subgroup_carrier_nonempty] Theorem
⊢ ∀g h. h ≤ g ⇒ H ≠ ∅
[subgroup_carrier_subset] Theorem
⊢ ∀g h. h ≤ g ⇒ H ⊆ G
[subgroup_conjugate_subgroup_bij] Theorem
⊢ ∀g h.
h ≤ g ⇒
∀a. a ∈ G ⇒
BIJ (λz. a * z * |/ a) H (conjugate_subgroup h g a).carrier
[subgroup_coset_card] Theorem
⊢ ∀g h. h ≤ g ∧ FINITE H ⇒ ∀a. a ∈ G ⇒ CARD (a * H) = CARD H
[subgroup_coset_card_partition_element] Theorem
⊢ ∀g h.
h ≤ g ∧ FINITE G ⇒
∀e. e ∈ partition (left_coset g H) G ⇒ CARD e = CARD H
[subgroup_coset_eq] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * H = y * H ⇔ |/ y * x ∈ H)
[subgroup_coset_in_partition] Theorem
⊢ ∀g h.
h ≤ g ⇒ ∀x. x ∈ IMAGE (left_coset g H) G ⇔ x ∈ CosetPartition g h
[subgroup_coset_nonempty] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ G ⇒ x ∈ x * H
[subgroup_coset_partition_element] Theorem
⊢ ∀g h.
h ≤ g ⇒
∀e. e ∈ partition (left_coset g H) G ⇔ ∃a. a ∈ G ∧ e = a * H
[subgroup_coset_subset] Theorem
⊢ ∀g h a x. h ≤ g ∧ a ∈ G ∧ x ∈ a * H ⇒ x ∈ G
[subgroup_coset_sym] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀a b. a ∈ G ∧ b ∈ G ∧ b ∈ a * H ⇒ a ∈ b * H
[subgroup_coset_trans] Theorem
⊢ ∀g h.
h ≤ g ⇒
∀a b c. a ∈ G ∧ b ∈ G ∧ c ∈ G ∧ b ∈ a * H ∧ c ∈ b * H ⇒ c ∈ a * H
[subgroup_cross_assoc] Theorem
⊢ ∀g h1 h2 h3.
h1 ≤ g ∧ h2 ≤ g ∧ h3 ≤ g ⇒ (h1 ∘ h2) ∘ h3 = h1 ∘ h2 ∘ h3
[subgroup_cross_card] Theorem
⊢ ∀g h1 h2.
h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
(let
s1 = h1.carrier;
s2 = h2.carrier
in
CARD (h1 ∘ h2).carrier = CARD s1 * CARD s2 DIV CARD (s1 ∩ s2))
[subgroup_cross_card_eqn] Theorem
⊢ ∀g h1 h2.
h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
(let
s1 = h1.carrier;
s2 = h2.carrier
in
CARD (h1 ∘ h2).carrier * CARD (s1 ∩ s2) = CARD s1 * CARD s2)
[subgroup_cross_closure_comm_assoc_fun] Theorem
⊢ ∀g. AbelianGroup g ⇒ closure_comm_assoc_fun $o (all_subgroups g)
[subgroup_cross_comm] Theorem
⊢ ∀g. AbelianGroup g ⇒ ∀h1 h2. h1 ≤ g ∧ h2 ≤ g ⇒ h1 ∘ h2 = h2 ∘ h1
[subgroup_cross_finite] Theorem
⊢ ∀g h1 h2.
h1 ≤ g ∧ h2 ≤ g ∧ h1 ∘ h2 = h2 ∘ h1 ∧ FiniteGroup h1 ∧
FiniteGroup h2 ⇒
FiniteGroup (h1 ∘ h2)
[subgroup_cross_group] Theorem
⊢ ∀g h1 h2. h1 ≤ g ∧ h2 ≤ g ∧ h1 ∘ h2 = h2 ∘ h1 ⇒ Group (h1 ∘ h2)
[subgroup_cross_property] Theorem
⊢ ∀g h1 h2.
(h1 ∘ h2).carrier = h1.carrier ∘ h2.carrier ∧ (h1 ∘ h2).op = $* ∧
(h1 ∘ h2).id = #e
[subgroup_cross_self] Theorem
⊢ ∀g h. h ≤ g ⇒ h ∘ h = h
[subgroup_cross_subgroup] Theorem
⊢ ∀g h1 h2. h1 ≤ g ∧ h2 ≤ g ∧ h1 ∘ h2 = h2 ∘ h1 ⇒ h1 ∘ h2 ≤ g
[subgroup_element] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀z. z ∈ H ⇒ z ∈ G
[subgroup_eq] Theorem
⊢ ∀g h1 h2. h1 ≤ g ∧ h2 ≤ g ⇒ (h1 = h2 ⇔ h1.carrier = h2.carrier)
[subgroup_eq_carrier] Theorem
⊢ ∀g h. h ≤ g ∧ H = G ⇒ h = g
[subgroup_eqn] Theorem
⊢ ∀g h. subgroup h g ⇔ H ⊆ G ∧ ∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y
[subgroup_exp] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ H ⇒ ∀n. h.exp x n = x ** n
[subgroup_groups] Theorem
⊢ ∀g h. h ≤ g ⇒ Group h ∧ Group g
[subgroup_has_groups] Theorem
⊢ ∀g h. h ≤ g ⇒ Group g ∧ Group h
[subgroup_homo_homo] Theorem
⊢ ∀g h k f. subgroup h g ∧ GroupHomo f g k ⇒ GroupHomo f h k
[subgroup_homomorphism] Theorem
⊢ ∀g h. h ≤ g ⇒ Group h ∧ Group g ∧ subgroup h g
[subgroup_id] Theorem
⊢ ∀g h. h ≤ g ⇒ #i = #e
[subgroup_incoset_equiv] Theorem
⊢ ∀g h. h ≤ g ⇒ left_coset g H equiv_on G
[subgroup_intersect_group] Theorem
⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ Group (h mINTER k)
[subgroup_intersect_has_inv] Theorem
⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ ∀x. x ∈ H ∩ K ⇒ |/ x ∈ H ∩ K
[subgroup_intersect_inv] Theorem
⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ ∀x. x ∈ H ∩ K ⇒ (h mINTER k).inv x = |/ x
[subgroup_intersect_property] Theorem
⊢ ∀g h k.
h ≤ g ∧ k ≤ g ⇒
(h mINTER k).carrier = H ∩ K ∧
(∀x y. x ∈ H ∩ K ∧ y ∈ H ∩ K ⇒ (h mINTER k).op x y = x * y) ∧
(h mINTER k).id = #e ∧ ∀x. x ∈ H ∩ K ⇒ (h mINTER k).inv x = |/ x
[subgroup_intersect_subgroup] Theorem
⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ (h mINTER k) ≤ g
[subgroup_inv] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ H ⇒ h.inv x = |/ x
[subgroup_inv_closure] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H
[subgroup_is_group] Theorem
⊢ ∀g h. h ≤ g ⇒ Group h
[subgroup_is_submonoid] Theorem
⊢ ∀g h. h ≤ g ⇒ h << g
[subgroup_is_submonoid0] Theorem
⊢ ∀g h. Group g ∧ Group h ∧ subgroup h g ⇒ submonoid h g
[subgroup_op] Theorem
⊢ ∀g h. h ≤ g ⇒ $o = $*
[subgroup_order] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ H ⇒ order h x = ord x
[subgroup_order_eqn] Theorem
⊢ ∀g h.
Group g ∧ Group h ∧ subgroup h g ⇒ ∀x. x ∈ H ⇒ order h x = ord x
[subgroup_property] Theorem
⊢ ∀g h.
h ≤ g ⇒ Group h ∧ Group g ∧ ∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y
[subgroup_property_all] Theorem
⊢ ∀g h.
h ≤ g ⇒
Group g ∧ Group h ∧ H ≠ ∅ ∧ H ⊆ G ∧ $o = $* ∧ #i = #e ∧
(∀x. x ∈ H ⇒ h.inv x = |/ x) ∧ ∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H
[subgroup_refl] Theorem
⊢ ∀g. Group g ⇒ g ≤ g
[subgroup_reflexive] Theorem
⊢ ∀g. subgroup g g
[subgroup_subset] Theorem
⊢ ∀g h. subgroup h g ⇒ H ⊆ G
[subgroup_test_by_cross] Theorem
⊢ ∀g. Group g ⇒
∀h. h ≤ g ⇔ H ≠ ∅ ∧ H ⊆ G ∧ h ∘ h = h ∧ IMAGE |/ H = H
[subgroup_thm] Theorem
⊢ ∀g h.
h ≤ g ⇔
Group g ∧ $o = $* ∧ #i = #e ∧ H ≠ ∅ ∧ H ⊆ G ∧
∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H
[subgroup_to_coset_bij] Theorem
⊢ ∀g h. h ≤ g ⇒ ∀a. a ∈ G ⇒ BIJ (λx. a * x) H (a * H)
[subgroup_trans] Theorem
⊢ ∀g h t. h ≤ t ∧ t ≤ g ⇒ h ≤ g
[subgroup_transitive] Theorem
⊢ ∀g h k. subgroup g h ∧ subgroup h k ⇒ subgroup g k
[subset_big_cross_empty] Theorem
⊢ ∀g. ssbcross ∅ = {#e}
[subset_big_cross_insert] Theorem
⊢ ∀g. FiniteAbelianGroup g ⇒
∀B. B ⊆ POW G ⇒
∀s. s ⊆ G ∧ s ∉ B ⇒ ssbcross (s INSERT B) = s ∘ ssbcross B
[subset_big_cross_thm] Theorem
⊢ ∀g. FiniteAbelianGroup g ⇒
∀B. B ⊆ POW G ⇒
∀s. s ⊆ G ⇒
ssbcross (s INSERT B) = s ∘ ssbcross (B DELETE s)
[subset_cross_alt] Theorem
⊢ ∀g s1 s2. s1 ∘ s2 = IMAGE (λ(x,y). x * y) (s1 × s2)
[subset_cross_assoc] Theorem
⊢ ∀g. Group g ⇒
∀s1 s2 s3.
s1 ⊆ G ∧ s2 ⊆ G ∧ s3 ⊆ G ⇒ (s1 ∘ s2) ∘ s3 = s1 ∘ s2 ∘ s3
[subset_cross_closure_comm_assoc_fun] Theorem
⊢ ∀g. AbelianGroup g ⇒ closure_comm_assoc_fun $o (POW G)
[subset_cross_comm] Theorem
⊢ ∀g. AbelianGroup g ⇒ ∀s1 s2. s1 ⊆ G ∧ s2 ⊆ G ⇒ s1 ∘ s2 = s2 ∘ s1
[subset_cross_element] Theorem
⊢ ∀g s1 s2 x y. x ∈ s1 ∧ y ∈ s2 ⇒ x * y ∈ s1 ∘ s2
[subset_cross_element_iff] Theorem
⊢ ∀g s1 s2 z. z ∈ s1 ∘ s2 ⇔ ∃x y. x ∈ s1 ∧ y ∈ s2 ∧ z = x * y
[subset_cross_element_preimage_card] Theorem
⊢ ∀g h1 h2.
h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
(let
s1 = h1.carrier;
s2 = h2.carrier;
f (x,y) = x * y
in
∀z. z ∈ s1 ∘ s2 ⇒
CARD (preimage f (s1 × s2) z) = CARD (s1 ∩ s2))
[subset_cross_finite] Theorem
⊢ ∀g s1 s2. FINITE s1 ∧ FINITE s2 ⇒ FINITE (s1 ∘ s2)
[subset_cross_inv] Theorem
⊢ ∀g. Group g ⇒
∀s1 s2.
s1 ⊆ G ∧ s2 ⊆ G ⇒
IMAGE |/ (s1 ∘ s2) = IMAGE |/ s2 ∘ IMAGE |/ s1
[subset_cross_partition_property] Theorem
⊢ ∀g h1 h2.
h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
(let
s1 = h1.carrier;
s2 = h2.carrier;
f (x,y) = x * y
in
∀t. t ∈ partition (feq f) (s1 × s2) ⇒ CARD t = CARD (s1 ∩ s2))
[subset_cross_preimage_inj] Theorem
⊢ ∀g s1 s2.
INJ (preimage (λ(x,y). x * y) (s1 × s2)) (s1 ∘ s2)
𝕌(:α # α -> bool)
[subset_cross_self] Theorem
⊢ ∀g h. h ≤ g ⇒ H ∘ H = H
[subset_cross_subset] Theorem
⊢ ∀g. Group g ⇒ ∀s1 s2. s1 ⊆ G ∧ s2 ⊆ G ⇒ s1 ∘ s2 ⊆ G
[subset_cross_to_preimage_cross_bij] Theorem
⊢ ∀g h1 h2.
h1 ≤ g ∧ h2 ≤ g ⇒
(let
s1 = h1.carrier;
s2 = h2.carrier;
f (x,y) = x * y
in
∀z. z ∈ s1 ∘ s2 ⇒
BIJ (λd. (left z * d,|/ d * right z)) (s1 ∩ s2)
(preimage f (s1 × s2) z))
[subset_group_exp] Theorem
⊢ ∀g s x. x ∈ s ⇒ ∀n. (subset_group g s).exp x n = x ** n
[subset_group_order] Theorem
⊢ ∀g s x. x ∈ s ⇒ order (subset_group g s) x = ord x
[subset_group_property] Theorem
⊢ ∀g s.
(subset_group g s).carrier = s ∧ (subset_group g s).op = $* ∧
(subset_group g s).id = #e
[subset_group_subgroup] Theorem
⊢ ∀g s.
Group g ∧ s ≠ ∅ ∧ s ⊆ G ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ x * |/ y ∈ s) ⇒
subset_group g s ≤ g
[subset_group_submonoid] Theorem
⊢ ∀g s.
Monoid g ∧ #e ∈ s ∧ s ⊆ G ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ x * y ∈ s) ⇒
subset_group g s << g
[subset_preimage_image] Theorem
⊢ ∀f g1 g2 h.
Group g1 ∧ Group g2 ∧ h ≤ g1 ∧ GroupHomo f g1 g2 ⇒
H ⊆ PREIMAGE f (IMAGE f H) ∩ g1.carrier
[sum_image_as_op_image] Theorem
⊢ ∑ = OP_IMAGE (λx y. x + y) 0
[symdiff_set_abelian_group] Theorem
⊢ AbelianGroup symdiff_set
[symdiff_set_group] Theorem
⊢ Group symdiff_set
[target_card_and_fixed_points_congruence] Theorem
⊢ ∀f g X n.
Group g ∧ (g act X) f ∧ FINITE X ∧ 0 < n ∧
(∀e. e ∈ multi_orbits f g X ⇒ CARD e = n) ⇒
CARD X MOD n = CARD (fixed_points f g X) MOD n
[target_card_by_fixed_points] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ∧ FINITE X ⇒
CARD X = CARD (fixed_points f g X) + ∑ CARD (multi_orbits f g X)
[target_card_by_orbit_types] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ∧ FINITE X ⇒
CARD X = CARD (sing_orbits f g X) + ∑ CARD (multi_orbits f g X)
[target_card_by_partition] Theorem
⊢ ∀f g X.
Group g ∧ (g act X) f ∧ FINITE X ⇒ CARD X = ∑ CARD (orbits f g X)
[target_orbits_disjoint] Theorem
⊢ ∀f g X. DISJOINT (sing_orbits f g X) (multi_orbits f g X)
[target_orbits_union] Theorem
⊢ ∀f g X. orbits f g X = sing_orbits f g X ∪ multi_orbits f g X
[trivial_group] Theorem
⊢ ∀e. FiniteAbelianGroup (trivial_group e)
[trivial_group_carrier] Theorem
⊢ ∀e. (trivial_group e).carrier = {e}
[trivial_group_id] Theorem
⊢ ∀e. (trivial_group e).id = e
*)
end
HOL 4, Trindemossen-2