Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-17 13:50 b454daed

View on Github →

feat(group_theory/perm): swap_mul_swal / swap_swap_apply (by @kckennylau)

Estimated changes

Modified data/nat/basic.lean

added theorem nat.pred_eq_of_eq_succ

Modified group_theory/perm.lean

modified theorem equiv.perm.eq_sign_of_surjective_hom

modified theorem equiv.perm.sign_aux3_symm_trans_trans

modified theorem equiv.perm.sign_bij

modified theorem equiv.perm.sign_eq_of_is_swap

modified theorem equiv.perm.sign_eq_sign_of_equiv

modified theorem equiv.perm.sign_inv

modified theorem equiv.perm.sign_mul

modified theorem equiv.perm.sign_of_subtype

modified theorem equiv.perm.sign_one

modified theorem equiv.perm.sign_prod_list_swap

added theorem equiv.perm.sign_refl

modified theorem equiv.perm.sign_subtype_perm

added theorem equiv.perm.sign_swap'

modified theorem equiv.perm.sign_swap

modified theorem equiv.perm.sign_symm_trans_trans

added theorem equiv.perm.swap_mul_self

added theorem equiv.perm.swap_swap_apply