Commit 2023-05-25 17:59 f8480be7

View on Github →

feat: port GroupTheory.SpecificGroups.Cyclic (#4316)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem CommGroup.is_simple_iff_isCyclic_and_prime_card

added theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers

added theorem IsAddCyclic.card_orderOf_eq_totient

added theorem IsCyclic.card_orderOf_eq_totient

added theorem IsCyclic.card_pow_eq_one_le

added def IsCyclic.commGroup

added theorem IsCyclic.exists_monoid_generator

added theorem IsCyclic.exponent_eq_card

added theorem IsCyclic.exponent_eq_zero_of_infinite

added theorem IsCyclic.iff_exponent_eq_card

added theorem IsCyclic.image_range_card

added theorem IsCyclic.image_range_orderOf

added theorem IsCyclic.of_exponent_eq_card

added theorem IsSimpleGroup.prime_card

added theorem MonoidHom.map_cyclic

added theorem card_orderOf_eq_totient_aux₂

added def commGroupOfCycleCenterQuotient

added theorem commutative_of_cyclic_center_quotient

added theorem isAddCyclic_of_card_pow_eq_one_le

added theorem isCyclic_of_card_pow_eq_one_le

added theorem isCyclic_of_orderOf_eq_card

added theorem isCyclic_of_prime_card

added theorem isSimpleGroup_of_prime_card

added theorem orderOf_eq_card_of_forall_mem_zpowers