Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-22 11:36 96f09a67

View on Github →

feat(group_theory/perm/cycles): cycle_factors_finset (#7540)

Estimated changes

Modified src/data/finset/noncomm_prod.lean

added theorem finset.noncomm_prod_singleton

Modified src/group_theory/perm/cycle_type.lean

deleted theorem equiv.perm.list_cycles_perm_list_cycles

deleted theorem equiv.perm.mem_list_cycles_iff

Modified src/group_theory/perm/cycles.lean

added def equiv.perm.cycle_factors_finset

added theorem equiv.perm.cycle_factors_finset_eq_empty_iff

added theorem equiv.perm.cycle_factors_finset_eq_finset

added theorem equiv.perm.cycle_factors_finset_eq_list_to_finset

added theorem equiv.perm.cycle_factors_finset_eq_singleton_iff

added theorem equiv.perm.cycle_factors_finset_eq_singleton_self_iff

added theorem equiv.perm.cycle_factors_finset_injective

added theorem equiv.perm.cycle_factors_finset_mem_commute

added theorem equiv.perm.cycle_factors_finset_noncomm_prod

added theorem equiv.perm.cycle_factors_finset_pairwise_disjoint

added theorem equiv.perm.is_cycle.eq_on_support_inter_nonempty_congr

added theorem equiv.perm.is_cycle.support_congr

added theorem equiv.perm.list_cycles_perm_list_cycles

added theorem equiv.perm.mem_cycle_factors_finset_iff

added theorem equiv.perm.mem_list_cycles_iff

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/perm/support.lean

added theorem equiv.perm.disjoint.commute

added theorem equiv.perm.disjoint.mem_imp

deleted theorem equiv.perm.disjoint.mul_comm

added theorem equiv.perm.disjoint.symmetric

added theorem equiv.perm.eq_on_support_mem_disjoint

added theorem equiv.perm.pow_eq_on_of_mem_support

modified theorem equiv.perm.support_congr

added theorem equiv.perm.support_le_prod_of_mem

Modified src/group_theory/specific_groups/alternating.lean