Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-30 00:53 09afe572

View on Github →

feat(group_theory/p_group): Groups of order p^2 are commutative (#8632)

Estimated changes

Modified src/group_theory/p_group.lean

modified theorem is_p_group.bot_lt_center

added theorem is_p_group.card_center_eq_prime_pow

modified theorem is_p_group.card_modeq_card_fixed_points

modified theorem is_p_group.center_nontrivial

added def is_p_group.comm_group_of_card_eq_prime_sq

added theorem is_p_group.commutative_of_card_eq_prime_sq

added theorem is_p_group.cyclic_center_quotient_of_card_eq_prime_sq

modified theorem is_p_group.index

modified theorem is_p_group.nonempty_fixed_point_of_prime_not_dvd_card

added theorem is_p_group.nontrivial_iff_card