Commit 2023-11-13 07:42 771e087d

View on Github →

chore: Generalise lemmas from finite groups to torsion elements (#8342) Many lemmas in GroupTheory.OrderOfElement were stated for elements of finite groups even though they work more generally for torsion elements of possibly infinite groups. This PR generalises those lemmas (and leaves convenience lemmas stated for finite groups), and fixes a bunch of names to use dot notation.

Renames

  • Function.eq_of_lt_minimalPeriod_of_iterate_eq → Function.iterate_injOn_Iio_minimalPeriod
  • Function.eq_iff_lt_minimalPeriod_of_iterate_eq → Function.iterate_eq_iterate_iff_of_lt_minimalPeriod
  • isOfFinOrder_iff_coe → Submonoid.isOfFinOrder_coe
  • orderOf_pos' → IsOfFinOrder.orderOf_pos
  • pow_eq_mod_orderOf → pow_mod_orderOf (and turned around)
  • pow_injective_of_lt_orderOf → pow_injOn_Iio_orderOf
  • mem_powers_iff_mem_range_order_of' → IsOfFinOrder.mem_powers_iff_mem_range_orderOf
  • orderOf_pow'' → IsOfFinOrder.orderOf_pow
  • orderOf_pow_coprime → Nat.Coprime.orderOf_pow
  • zpow_eq_mod_orderOf → zpow_mod_orderOf (and turned around)
  • exists_pow_eq_one → isOfFinOrder_of_finite
  • pow_apply_eq_pow_mod_orderOf_cycleOf_apply → pow_mod_orderOf_cycleOf_apply

New lemmas

  • IsOfFinOrder.powers_eq_image_range_orderOf
  • IsOfFinOrder.natCard_powers_le_orderOf
  • IsOfFinOrder.finite_powers
  • finite_powers
  • infinite_powers
  • Nat.card_submonoidPowers
  • IsOfFinOrder.mem_powers_iff_mem_zpowers
  • IsOfFinOrder.powers_eq_zpowers
  • IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf
  • IsOfFinOrder.exists_pow_eq_one

Other changes

  • Move decidableMemPowers/fintypePowers to GroupTheory.Submonoid.Membership and decidableMemZpowers/fintypeZpowers to GroupTheory.Subgroup.ZPowers.
  • finEquivPowers, finEquivZpowers, powersEquivPowers and zpowersEquivZpowers now assume IsOfFinTorsion x instead of Finite G.
  • isOfFinOrder_iff_pow_eq_one now takes one less explicit argument.
  • Delete Equiv.Perm.IsCycle.exists_pow_eq_one since it was saying that a permutation over a finite type is torsion, but this is trivial since the group of permutation is itself finite, so we can use isOfFinOrder_of_finite instead.

Estimated changes

modified theorem Function.minimalPeriod_id
deleted theorem IsOfFinOrder.inv
deleted theorem exists_pow_eq_one
modified theorem exists_zpow_eq_one
modified theorem finEquivPowers_apply
modified theorem finEquivPowers_symm_apply
modified theorem finEquivZpowers_apply
modified theorem finEquivZpowers_symm_apply
added theorem finite_powers
added theorem infinite_powers
deleted theorem isOfFinOrder_iff_coe
modified theorem isOfFinOrder_iff_pow_eq_one
modified theorem isOfFinOrder_inv_iff
modified theorem isOfFinOrder_ofAdd_iff
added theorem isOfFinOrder_of_finite
modified theorem mem_powers_iff_mem_zpowers
modified theorem orderOf_eq_card_powers
modified theorem orderOf_ofAdd_eq_addOrderOf
deleted theorem orderOf_pos'
modified theorem orderOf_pos
deleted theorem orderOf_pow''
modified theorem orderOf_pow
deleted theorem orderOf_pow_coprime
deleted theorem pow_eq_mod_orderOf
added theorem pow_injOn_Iio_orderOf
modified theorem pow_inj_mod
added theorem pow_mod_orderOf
modified theorem powersEquivPowers_apply
modified theorem powers_eq_zpowers
deleted theorem zpow_eq_mod_orderOf
added theorem zpow_mod_orderOf
modified theorem zpowersEquivZpowers_apply