Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-16 09:30 0c2c2bdd

View on Github →

feat(group_theory/perm/cycles): cycle_factors (#815)

Estimated changes

Created src/group_theory/perm/cycles.lean

added theorem equiv.perm.apply_eq_self_iff_of_same_cycle

added def equiv.perm.cycle_factors

added def equiv.perm.cycle_factors_aux

added def equiv.perm.cycle_of

added theorem equiv.perm.cycle_of_apply

added theorem equiv.perm.cycle_of_apply_of_not_same_cycle

added theorem equiv.perm.cycle_of_apply_of_same_cycle

added theorem equiv.perm.cycle_of_apply_self

added theorem equiv.perm.cycle_of_cycle

added theorem equiv.perm.cycle_of_gpow_apply_self

added theorem equiv.perm.cycle_of_inv

added theorem equiv.perm.cycle_of_one

added theorem equiv.perm.cycle_of_pow_apply_self

added theorem equiv.perm.is_cycle_cycle_of

added theorem equiv.perm.same_cycle.refl

added theorem equiv.perm.same_cycle.symm

added theorem equiv.perm.same_cycle.trans

added def equiv.perm.same_cycle

added theorem equiv.perm.same_cycle_apply

added theorem equiv.perm.same_cycle_cycle

added theorem equiv.perm.same_cycle_inv

added theorem equiv.perm.same_cycle_inv_apply

added theorem equiv.perm.same_cycle_of_is_cycle

Renamed src/group_theory/perm.lean to src/group_theory/perm/sign.lean

added theorem equiv.perm.card_support_swap_mul

added theorem equiv.perm.disjoint.symm

added def equiv.perm.disjoint

added theorem equiv.perm.disjoint_comm

added theorem equiv.perm.disjoint_mul_comm

added theorem equiv.perm.disjoint_mul_left

added theorem equiv.perm.disjoint_mul_right

added theorem equiv.perm.disjoint_one_left

added theorem equiv.perm.disjoint_one_right

added theorem equiv.perm.disjoint_prod_perm

added theorem equiv.perm.disjoint_prod_right

added theorem equiv.perm.exists_gpow_eq_of_is_cycle

deleted theorem equiv.perm.exists_int_pow_eq_of_is_cycle

added theorem equiv.perm.gpow_apply_eq_of_apply_apply_eq_self

added theorem equiv.perm.gpow_apply_eq_self_of_apply_eq_self

modified def equiv.perm.is_cycle

modified theorem equiv.perm.is_cycle_inv

added theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self

added theorem equiv.perm.of_subtype_one

added theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self

deleted theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self_int

deleted theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self_nat

added theorem equiv.perm.pow_apply_eq_self_of_apply_eq_self

added theorem equiv.perm.subtype_perm_one

deleted theorem equiv.perm.support_swap_mul

deleted theorem equiv.perm.support_swap_mul_cycle

added theorem equiv.perm.support_swap_mul_eq

added theorem equiv.perm.swap_induction_on

Modified src/linear_algebra/determinant.lean

Modified test/fin_cases.lean