Commit 2023-02-27 16:19 5d95a0a0

View on Github →

feat: port GroupTheory.Perm.Option (#2523)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/Option.lean

added def Equiv.Perm.decomposeOption

added theorem Equiv.Perm.decomposeOption_symm_of_none_apply

added theorem Equiv.Perm.decomposeOption_symm_sign

added theorem Equiv.optionCongr_one

added theorem Equiv.optionCongr_sign

added theorem Equiv.optionCongr_swap

added theorem Finset.univ_perm_option

added theorem map_equiv_removeNone