Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-24 11:57 76b1e012

View on Github →

feat(data/equiv/option): option_congr (#12263) This is a universe-polymorphic version of the existing equiv_functor.map_equiv option.

Estimated changes

Modified src/combinatorics/derangements/basic.lean

Modified src/data/equiv/option.lean

added def equiv.option_congr

added theorem equiv.option_congr_eq_equiv_function_map_equiv

added theorem equiv.option_congr_injective

added theorem equiv.option_congr_refl

added theorem equiv.option_congr_symm

added theorem equiv.option_congr_trans

deleted theorem equiv.remove_none_map_equiv

added theorem equiv.remove_none_option_congr

Modified src/group_theory/perm/option.lean

added theorem equiv.option_congr_one

added theorem equiv.option_congr_sign

added theorem equiv.option_congr_swap

deleted theorem equiv_functor.map_equiv_option_injective

deleted theorem equiv_functor.option.map_none

deleted theorem equiv_functor.option.sign

deleted theorem map_equiv_option_one

deleted theorem map_equiv_option_refl

deleted theorem map_equiv_option_swap