Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-14 14:48 667dcf37

View on Github →

feat(group_theory/sylow): first sylow theorem (closes #591)

Estimated changes

Modified group_theory/group_action.lean

added theorem is_group_action.comp_hom

added def is_group_action.mul_left_cosets

added theorem is_monoid_action.comp_hom

Modified group_theory/sylow.lean

added theorem sylow.exists_subgroup_card_pow_prime

added theorem sylow.fixed_points_mul_left_cosets_equiv_quotient

added theorem sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizer