Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.perm.decompose_fin_symm_of_refl

Modification history

2021-02-16 12:05
src/group_theory/perm/fin.lean
feat(data/equiv): Add lemmas to reduce `@finset.univ (perm (fin n.succ)) _` (#5593) …
Added equiv.perm.decompose_fin_symm_of_reflView on Github →