Commit 2021-09-13 09:34 a8a8edcb

View on Github →

feat(group_theory/p_group): Generalize to infinite p-groups (#9082) Defines p-groups, and generalizes the results of p_group.lean to infinite p-groups. The eventual goal is to generalize Sylow's theorems to infinite groups.

Estimated changes

Modified src/group_theory/p_group.lean

added theorem is_p_group.card_orbit

added theorem is_p_group.iff_card

added theorem is_p_group.iff_order_of

added theorem is_p_group.index

added theorem is_p_group.of_card

added theorem is_p_group.to_le

added theorem is_p_group.to_quotient

added theorem is_p_group.to_subgroup

added def is_p_group

modified theorem mul_action.nonempty_fixed_point_of_prime_not_dvd_card

Modified src/group_theory/sylow.lean