Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-12 07:04 c550e3a3

View on Github →

refactor(group_theory/sylow): make new file about actions of p groups and move lemmas there (#8595)

Estimated changes

Modified src/group_theory/group_action/basic.lean

added theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one

Created src/group_theory/p_group.lean

added theorem mul_action.card_modeq_card_fixed_points

added theorem mul_action.exists_fixed_point_of_prime_dvd_card_of_fixed_point

added theorem mul_action.nonempty_fixed_point_of_prime_not_dvd_card

Modified src/group_theory/sylow.lean

deleted theorem mul_action.card_modeq_card_fixed_points

deleted theorem mul_action.exists_fixed_point_of_prime_dvd_card_of_fixed_point

deleted theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one

deleted theorem mul_action.nonempty_fixed_point_of_prime_not_dvd_card