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