Mathlib Changelog
Changelog
About
Github
Commit
2018-03-10 13:38
b97b7c38
View on Github →
feat(group_theory): add a little bit of group theory; prove of Lagrange's theorem
Estimated changes
Modified
data/equiv.lean
added
def
equiv.subtype_subtype_equiv_subtype
Modified
data/finset.lean
added
theorem
finset.card_attach
added
theorem
finset.card_eq_of_bijective
added
theorem
finset.card_le_card_of_inj_on
added
theorem
finset.card_le_of_inj_on
Modified
data/fintype.lean
added
def
fintype.fintype_prod_left
added
def
fintype.fintype_prod_right
Modified
data/int/basic.lean
Modified
data/multiset.lean
added
theorem
multiset.card_attach
Modified
data/set/finite.lean
added
theorem
set.infinite_univ_nat
added
theorem
set.not_injective_int_fintype
added
theorem
set.not_injective_nat_fintype
Created
group_theory/subgroup.lean
added
def
cosets
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
is_subgroup.Union_cosets_eq_univ
added
theorem
is_subgroup.cosets_disjoint
added
theorem
is_subgroup.cosets_equiv_subgroup
added
theorem
is_subgroup.group_equiv_cosets_times_subgroup
added
theorem
is_subgroup.injective_mul
added
theorem
is_subgroup.inv_mem
added
theorem
is_subgroup.inv_mem_iff
added
theorem
is_subgroup.mul_image
added
theorem
is_subgroup.mul_mem
added
theorem
is_subgroup.pairwise_cosets_disjoint
added
theorem
is_subgroup.subgroup_mem_cosets
added
structure
is_subgroup
added
theorem
is_subgroup_range_gpow
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
set_theory/cardinal.lean