Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-01 00:19 6c617793

View on Github →

refactor(group_theory/order_of_element): use minimal_period for the definition (#7082) This PR redefines order_of_element in terms of function.minimal_period. It furthermore introduces a predicate on elements of a finite group to be of finite order. Co-authored by: Damiano Testa adomani@gmail.com

Estimated changes

added theorem mul_one_eq_id
added theorem one_mul_eq_id
modified theorem add_left_iterate
modified theorem add_right_iterate
modified theorem mul_left_iterate
modified theorem mul_right_iterate
modified theorem add_order_of_dvd_card_univ
modified theorem add_order_of_eq_one_iff
modified theorem add_order_of_eq_prime
modified theorem add_order_of_eq_prime_pow
deleted theorem add_order_of_eq_zero
modified theorem add_order_of_injective
modified theorem add_order_of_le_card_univ
modified theorem add_order_of_nsmul''
modified theorem add_order_of_nsmul
modified theorem add_order_of_nsmul_eq_zero
deleted theorem add_order_of_pos'
modified theorem add_order_of_pos
modified theorem add_order_of_zero
modified theorem card_nsmul_eq_zero
modified theorem exists_gpow_eq_one
modified theorem exists_gsmul_eq_zero
modified theorem exists_nsmul_eq_zero
modified theorem exists_pow_eq_one
modified theorem fin_equiv_gmultiples_apply
modified theorem fin_equiv_gpowers_apply
modified theorem fin_equiv_multiples_apply
modified theorem fin_equiv_powers_apply
modified theorem fin_equiv_powers_symm_apply
modified theorem gcd_nsmul_card_eq_zero_iff
modified theorem gpow_eq_mod_order_of
modified theorem gpowers_equiv_gpowers_apply
modified theorem gsmul_eq_mod_add_order_of
modified theorem image_range_add_order_of
modified theorem image_range_order_of
added def is_of_fin_order
modified theorem mem_powers_iff_mem_gpowers
modified theorem multiples_eq_gmultiples
modified theorem nsmul_eq_mod_add_order_of
modified theorem order_eq_card_gpowers
modified theorem order_eq_card_powers
modified theorem order_of_dvd_card_univ
modified theorem order_of_dvd_iff_pow_eq_one
modified theorem order_of_dvd_of_pow_eq_one
modified theorem order_of_eq_one_iff
modified theorem order_of_eq_order_of_iff
modified theorem order_of_eq_prime
modified theorem order_of_eq_prime_pow
modified theorem order_of_eq_zero
modified theorem order_of_injective
modified theorem order_of_le_card_univ
modified theorem order_of_le_of_pow_eq_one
modified theorem order_of_one
modified theorem order_of_pos'
modified theorem order_of_pos
modified theorem order_of_pow''
modified theorem order_of_pow
modified theorem order_of_subgroup
modified theorem order_of_submonoid
modified theorem pow_card_eq_one
modified theorem pow_eq_mod_order_of
modified theorem pow_gcd_card_eq_one_iff
modified theorem pow_injective_aux
modified theorem pow_order_of_eq_one
modified theorem powers_eq_gpowers
modified theorem powers_equiv_powers_apply