Mathlib v3 is deprecated. Go to Mathlib v4

Theorem map_equiv_remove_none

Modification history

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 map_equiv_remove_none View on Github →