Commit 2023-02-22 16:34 6cd62a5d

View on Github →

feat: port GroupTheory.OrderOfElement (#2279)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/OrderOfElement.lean

added theorem Commute.isOfFinOrder_mul

added theorem Commute.orderOf_dvd_lcm_mul

added theorem Commute.orderOf_mul_dvd_lcm

added theorem Commute.orderOf_mul_dvd_mul_orderOf

added theorem Commute.orderOf_mul_eq_mul_orderOf_of_coprime

added theorem Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd

added theorem IsOfFinOrder.apply

added theorem IsOfFinOrder.inv

added theorem IsOfFinOrder.mul

added theorem IsOfFinOrder.of_mem_zpowers

added theorem IsOfFinOrder.zpow

added def IsOfFinOrder

added theorem LinearOrderedRing.orderOf_le_two

added theorem MonoidHom.isOfFinOrder

added theorem Subgroup.pow_index_mem

added theorem addOrderOf_ofMul_eq_orderOf

added theorem exists_orderOf_eq_prime_pow_iff

added theorem exists_pow_eq_one

added theorem exists_pow_eq_self_of_coprime

added theorem exists_zpow_eq_one

added theorem finEquivPowers_apply

added theorem finEquivPowers_symm_apply

added theorem finEquivZpowers_apply

added theorem finEquivZpowers_symm_apply

added theorem image_range_orderOf

added theorem inf_eq_bot_of_coprime

added theorem infinite_not_isOfFinOrder

added theorem injective_pow_iff_not_isOfFinOrder

added theorem isOfFinAddOrder_ofMul_iff

added theorem isOfFinOrder_iff_coe

added theorem isOfFinOrder_iff_pow_eq_one

added theorem isOfFinOrder_inv_iff

added theorem isOfFinOrder_ofAdd_iff

added theorem isOfFinOrder_one

added theorem isPeriodicPt_mul_iff_pow_eq_one

added theorem mem_powers_iff_mem_range_orderOf

added theorem mem_powers_iff_mem_range_order_of'

added theorem mem_powers_iff_mem_zpowers

added theorem mem_zpowers_iff_mem_range_orderOf

added theorem not_isOfFinOrder_of_injective_pow

added theorem orderOf_abs_ne_one

added theorem orderOf_dvd_card_univ

added theorem orderOf_dvd_iff_pow_eq_one

added theorem orderOf_dvd_iff_zpow_eq_one

added theorem orderOf_dvd_nat_card

added theorem orderOf_dvd_of_mem_zpowers

added theorem orderOf_dvd_of_pow_eq_one

added theorem orderOf_eq_card_powers

added theorem orderOf_eq_card_zpowers

added theorem orderOf_eq_iff

added theorem orderOf_eq_of_pow_and_pow_div_prime

added theorem orderOf_eq_one_iff

added theorem orderOf_eq_orderOf_iff

added theorem orderOf_eq_prime

added theorem orderOf_eq_prime_pow

added theorem orderOf_eq_zero

added theorem orderOf_eq_zero_iff'

added theorem orderOf_eq_zero_iff

added theorem orderOf_injective

added theorem orderOf_inv

added theorem orderOf_le_card_univ

added theorem orderOf_le_of_pow_eq_one

added theorem orderOf_map_dvd

added theorem orderOf_ofAdd_eq_addOrderOf

added theorem orderOf_one

added theorem orderOf_pos'

added theorem orderOf_pos

added theorem orderOf_pos_iff

added theorem orderOf_pow''

added theorem orderOf_pow'

added theorem orderOf_pow

added theorem orderOf_pow_coprime

added theorem orderOf_pow_dvd

added theorem orderOf_subgroup

added theorem orderOf_submonoid

added theorem orderOf_units

added def powCardSubgroup

added theorem powCoprime_inv

added theorem powCoprime_one

added theorem pow_card_eq_one'

added theorem pow_card_eq_one

added theorem pow_eq_mod_card

added theorem pow_eq_mod_orderOf

added theorem pow_eq_one_iff_modEq

added theorem pow_eq_pow_iff_modEq

added theorem pow_gcd_card_eq_one_iff

added theorem pow_inj_iff_of_orderOf_eq_zero

added theorem pow_inj_mod

added theorem pow_injective_of_lt_orderOf

added theorem pow_ne_one_of_lt_orderOf'

added theorem pow_orderOf_eq_one

added theorem powersEquivPowers_apply

added theorem powers_eq_zpowers

added theorem smul_eq_self_of_mem_zpowers

added def subgroupOfIdempotent

added def submonoidOfIdempotent

added theorem sum_card_orderOf_eq_card_pow_eq_one

added theorem vadd_eq_self_of_mem_zmultiples

added theorem zpow_eq_mod_card

added theorem zpow_eq_mod_orderOf

added theorem zpow_pow_orderOf

added theorem zpowersEquivZpowers_apply

Modified Mathlib/Tactic/ToAdditive.lean