Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-11 14:49 fea24916

View on Github →

chore(group_theory): move order_of into its own file; base costes on left_coset

Estimated changes

Modified group_theory/coset.lean

added theorem is_subgroup.Union_left_cosets_eq_univ

added theorem is_subgroup.group_equiv_left_cosets_times_subgroup

added theorem is_subgroup.left_cosets_disjoint

added theorem is_subgroup.left_cosets_equiv_subgroup

added theorem is_subgroup.pairwise_left_cosets_disjoint

added theorem is_subgroup.subgroup_mem_left_cosets

modified def left_coset

modified theorem left_coset_assoc

modified def left_coset_equiv

modified theorem left_coset_equiv_rel

modified theorem left_coset_mem_left_coset

modified theorem left_coset_right_coset

added def left_cosets

modified theorem mem_left_coset

modified theorem mem_left_coset_iff

modified theorem mem_left_coset_left_coset

modified theorem mem_own_left_coset

modified theorem mem_own_right_coset

modified theorem mem_right_coset

modified theorem mem_right_coset_iff

modified theorem mem_right_coset_right_coset

modified theorem normal_of_eq_cosets

modified def right_coset

modified theorem right_coset_assoc

modified theorem right_coset_mem_right_coset

Created group_theory/order_of_element.lean

added theorem exists_gpow_eq_one

added theorem exists_pow_eq_one

added theorem finset.mem_range_iff_mem_finset_range_of_mod_eq

added theorem gpow_eq_mod_order_of

added theorem mem_range_gpow_iff_mem_range_order_of

added theorem order_eq_card_range_gpow

added def order_of

added theorem order_of_dvd_card_univ

added theorem order_of_le_card_univ

added theorem order_of_ne_zero

added theorem pow_eq_mod_order_of

added theorem pow_injective_of_lt_order_of

added theorem pow_order_of_eq_one

Modified group_theory/subgroup.lean

deleted def cosets

deleted theorem exists_gpow_eq_one

deleted theorem exists_pow_eq_one

deleted theorem finset.mem_range_iff_mem_finset_range_of_mod_eq

deleted theorem gpow_eq_mod_order_of

modified theorem injective_mul

deleted theorem is_subgroup.Union_cosets_eq_univ

deleted theorem is_subgroup.cosets_disjoint

deleted theorem is_subgroup.cosets_equiv_subgroup

deleted theorem is_subgroup.group_equiv_cosets_times_subgroup

deleted theorem is_subgroup.mul_image

deleted theorem is_subgroup.pairwise_cosets_disjoint

deleted theorem is_subgroup.subgroup_mem_cosets

deleted theorem mem_range_gpow_iff_mem_range_order_of

deleted theorem order_eq_card_range_gpow

deleted def order_of

deleted theorem order_of_dvd_card_univ

deleted theorem order_of_le_card_univ

deleted theorem order_of_ne_zero

deleted theorem pow_eq_mod_order_of

deleted theorem pow_injective_of_lt_order_of

deleted theorem pow_order_of_eq_one