Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-19 11:24 318ec36d

View on Github →

feat(group_theory/perm): sign_cycle and sign_bij (#347)

Estimated changes

Modified algebra/group_power.lean

added theorem int.units_pow_eq_pow_mod_two

added theorem int.units_pow_two

Modified data/equiv/basic.lean

modified theorem equiv.swap_apply_left

modified theorem equiv.swap_apply_right

modified theorem equiv.swap_swap

Modified group_theory/perm.lean

added theorem equiv.perm.card_support_swap

added theorem equiv.perm.eq_inv_iff_eq

added theorem equiv.perm.eq_swap_of_is_cycle_of_apply_apply_eq_self

added theorem equiv.perm.exists_int_pow_eq_of_is_cycle

added theorem equiv.perm.inv_eq_iff_eq

added def equiv.perm.is_cycle

added theorem equiv.perm.is_cycle_inv

added theorem equiv.perm.is_cycle_swap

added theorem equiv.perm.is_cycle_swap_mul

added theorem equiv.perm.is_cycle_swap_mul_aux₁

added theorem equiv.perm.is_cycle_swap_mul_aux₂

added theorem equiv.perm.is_swap_of_subtype

added theorem equiv.perm.mem_iff_of_subtype_apply_mem

added theorem equiv.perm.mem_support

added theorem equiv.perm.mul_swap_eq_swap_mul

added def equiv.perm.of_subtype

added theorem equiv.perm.of_subtype_apply_of_not_mem

added theorem equiv.perm.of_subtype_subtype_perm

added theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self_int

added theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self_nat

added theorem equiv.perm.sign_aux3_symm_trans_trans

added theorem equiv.perm.sign_bij

added theorem equiv.perm.sign_cycle

added theorem equiv.perm.sign_eq_sign_of_equiv

added theorem equiv.perm.sign_inv

added theorem equiv.perm.sign_mul

added theorem equiv.perm.sign_of_subtype

added theorem equiv.perm.sign_one

added theorem equiv.perm.sign_prod_list_swap

added theorem equiv.perm.sign_subtype_perm

added theorem equiv.perm.sign_symm_trans_trans

added def equiv.perm.subtype_perm

added theorem equiv.perm.subtype_perm_of_subtype

added def equiv.perm.support

added theorem equiv.perm.support_swap

added theorem equiv.perm.support_swap_mul_cycle

added theorem equiv.perm.swap_mul_eq_mul_swap