Commit 2023-01-27 14:02 cf20e0cb

View on Github →

feat: port GroupTheory.Perm.List (#1631)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/List.lean

added def List.formPerm

added theorem List.formPerm_apply_getLast

added theorem List.formPerm_apply_head

added theorem List.formPerm_apply_lt

added theorem List.formPerm_apply_mem_eq_self_iff

added theorem List.formPerm_apply_mem_ne_self_iff

added theorem List.formPerm_apply_mem_of_mem

added theorem List.formPerm_apply_nthLe

added theorem List.formPerm_apply_nthLe_length

added theorem List.formPerm_apply_nthLe_zero

added theorem List.formPerm_apply_of_not_mem

added theorem List.formPerm_cons_concat_apply_last

added theorem List.formPerm_cons_cons

added theorem List.formPerm_eq_formPerm_iff

added theorem List.formPerm_eq_head_iff_eq_getLast

added theorem List.formPerm_eq_of_isRotated

added theorem List.formPerm_eq_one_iff

added theorem List.formPerm_eq_self_of_not_mem

added theorem List.formPerm_ext_iff

added theorem List.formPerm_mem_iff_mem

added theorem List.formPerm_nil

added theorem List.formPerm_pair

added theorem List.formPerm_pow_apply_head

added theorem List.formPerm_pow_apply_nthLe

added theorem List.formPerm_pow_length_eq_one_of_nodup

added theorem List.formPerm_reverse

added theorem List.formPerm_rotate

added theorem List.formPerm_rotate_one

added theorem List.formPerm_singleton

added theorem List.form_perm_zpow_apply_mem_imp_mem

added theorem List.mem_of_formPerm_apply_mem

added theorem List.mem_of_formPerm_apply_ne

added theorem List.mem_of_formPerm_ne_self

added theorem List.support_formPerm_le'

added theorem List.support_formPerm_le

added theorem List.support_formPerm_of_nodup'

added theorem List.support_formPerm_of_nodup

added theorem List.zipWith_swap_prod_support'

added theorem List.zipWith_swap_prod_support