Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-09 09:53 7ed091df

View on Github →

feat(group_theory/perm/concrete_cycle): computable cyclic perm notation (#9470)

Estimated changes

Modified src/group_theory/perm/concrete_cycle.lean

added theorem equiv.perm.is_cycle.exists_unique_cycle_nontrivial_subtype

added def equiv.perm.iso_cycle'

added def equiv.perm.iso_cycle

added theorem equiv.perm.nodup_to_cycle

added theorem equiv.perm.nontrivial_to_cycle

added def equiv.perm.to_cycle

added theorem equiv.perm.to_cycle_eq_to_list