Commit 2023-05-25 20:21 7e67446e

View on Github →

feat: port GroupTheory.PGroup (#4318)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/PGroup.lean

added theorem IsPGroup.bot_lt_center

added theorem IsPGroup.card_center_eq_prime_pow

added theorem IsPGroup.card_eq_or_dvd

added theorem IsPGroup.card_modEq_card_fixedPoints

added theorem IsPGroup.card_orbit

added theorem IsPGroup.center_nontrivial

added theorem IsPGroup.comap_of_injective

added theorem IsPGroup.comap_of_ker_isPGroup

added theorem IsPGroup.comap_subtype

added def IsPGroup.commGroupOfCardEqPrimeSq

added theorem IsPGroup.commutative_of_card_eq_prime_sq

added theorem IsPGroup.coprime_card_of_ne

added theorem IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq

added theorem IsPGroup.disjoint_of_ne

added theorem IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point

added theorem IsPGroup.iff_card

added theorem IsPGroup.iff_orderOf

added theorem IsPGroup.index

added theorem IsPGroup.ker_isPGroup_of_injective

added theorem IsPGroup.map

added theorem IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card

added theorem IsPGroup.nontrivial_iff_card

added theorem IsPGroup.of_bot

added theorem IsPGroup.of_card

added theorem IsPGroup.of_equiv

added theorem IsPGroup.of_injective

added theorem IsPGroup.of_surjective

added theorem IsPGroup.orderOf_coprime

added theorem IsPGroup.powEquiv_apply

added theorem IsPGroup.powEquiv_symm_apply

added theorem IsPGroup.to_inf_left

added theorem IsPGroup.to_inf_right

added theorem IsPGroup.to_le

added theorem IsPGroup.to_quotient

added theorem IsPGroup.to_subgroup

added theorem IsPGroup.to_sup_of_normal_left'

added theorem IsPGroup.to_sup_of_normal_left

added theorem IsPGroup.to_sup_of_normal_right'

added theorem IsPGroup.to_sup_of_normal_right

added def IsPGroup