Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv_functor.map_equiv_option_injective

Modification history

2022-02-24 11:57
src/group_theory/perm/option.lean
feat(data/equiv/option): option_congr (#12263) …
Deleted equiv_functor.map_equiv_option_injectiveView on Github →
2021-02-16 12:05
src/group_theory/perm/option.lean
feat(data/equiv): Add lemmas to reduce `@finset.univ (perm (fin n.succ)) _` (#5593) …
Added equiv_functor.map_equiv_option_injectiveView on Github →