Mathlib Changelog
Changelog
About
Github
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