Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.perm

Modification history

2022-10-18 21:51

src/logic/equiv/basic.lean

chore(logic/equiv/basic): split into two files (#17038) …

Modified equiv.perm View on Github →

2022-03-07 12:17

src/data/equiv/basic.lean

chore(data/equiv/basic): rename `involutive.to_equiv` to `to_perm` (#12486)

Modified equiv.perm View on Github →

2017-09-08 14:49

data/equiv.lean

feat(data/equiv): port data/equiv.lean from Lean2

Added equiv.perm View on Github →