Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-13 19:02 b03c0aac

View on Github →

feat(group_theory/sylow): Cauchy's theorem (#458)

feat(group_theory): adding add_subgroup and add_submonoid
feat(data/list/basic): rotate a list

Estimated changes

Modified data/equiv/basic.lean

added theorem equiv.subtype_quotient_equiv_quotient_subtype

Modified group_theory/coset.lean

Modified group_theory/group_action.lean

added def is_group_action.orbit_rel

Created group_theory/sylow.lean

added theorem is_group_action.card_modeq_card_fixed_points

added theorem is_group_action.mem_fixed_points_iff_card_orbit_eq_one

added theorem quotient_group.card_preimage_mk

added theorem sylow.exists_prime_order_of_dvd_card

added theorem sylow.mem_vectors_prod_eq_one

added theorem sylow.mem_vectors_prod_eq_one_iff

added def sylow.mk_vector_prod_eq_one

added theorem sylow.mk_vector_prod_eq_one_inj

added theorem sylow.one_mem_fixed_points_rotate

added theorem sylow.one_mem_vectors_prod_eq_one

added def sylow.rotate_vectors_prod_eq_one

added def sylow.vectors_prod_eq_one