Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-04 22:44 d1723c04

View on Github →

refactor(group_theory/perm/cycle/basic): Consolidate API (#17898) Reorganise and complete the cycle API:

  • Previously, is_cycle was spelling out the definition of same_cycle. Now use it explicitly.
  • Change binder to semi-implicit in the definition of is_cycle.
  • Add lemmas and iff aliases.
  • Golf existing proofs using those (mostly invisible from the diff because git decided I am moving the is_cycle API)
  • Improve lemma names, mostly for better dot notation.

New lemmas

  • maps_to.extend_domain
  • surj_on.extend_domain
  • bij_on.extend_domain
  • extend_domain_pow
  • extend_domain_zpow
  • same_cycle.rfl
  • eq.same_cycle
  • same_cycle.conj
  • same_cycle_conj
  • same_cycle_pow_right_iff
  • same_cycle_zpow_right_iff
  • same_cycle.pow_left
  • same_cycle.pow_right
  • same_cycle.zpow_left
  • same_cycle.zpow_left
  • same_cycle.of_pow
  • same_cycle.of_zpow
  • same_cycle_subtype_perm
  • same_cycle.subtype_perm
  • same_cycle_extend_domain
  • is_cycle.conj
  • is_cycle.pow_eq_one_iff'
  • is_cycle.pow_eq_one_iff''

Renames

  • order_of_is_cycle → is_cycle.order_of
  • is_cycle.is_cycle_conj → is_cycle.conj
  • is_cycle_of_is_cycle_pow → is_cycle.of_pow
  • is_cycle_of_is_cycle_zpow → is_cycle.of_zpow
  • same_cycle_cycle → is_cycle_iff_same_cycle
  • mem_support_pos_pow_iff_of_lt_order_of → support_pow_of_pos_of_lt_order_of and change the statement to talk about unextensionalised finset equality

Estimated changes

modified def equiv.perm.cycle_of
modified theorem equiv.perm.cycle_of_apply
modified theorem equiv.perm.cycle_of_inv
modified theorem equiv.perm.cycle_of_one
modified theorem equiv.perm.is_cycle.inv
modified theorem equiv.perm.is_cycle.ne_one
modified def equiv.perm.is_cycle
modified theorem equiv.perm.is_cycle_swap
modified theorem equiv.perm.not_is_cycle_one
modified theorem equiv.perm.same_cycle.refl
modified def equiv.perm.same_cycle
modified theorem equiv.perm.same_cycle_inv