Mathlib v3 is deprecated. Go to Mathlib v4

Def function.involutive.to_equiv

Modification history

2022-03-07 12:17
src/data/equiv/basic.lean
chore(data/equiv/basic): rename `involutive.to_equiv` to `to_perm` (#12486)
Deleted function.involutive.to_equivView on Github →
2020-03-31 08:35
src/data/equiv/basic.lean
refactor(*): migrate more files to bundled `ring_hom`s (#2286) …
Modified function.involutive.to_equivView on Github →
2019-09-27 11:47
src/data/equiv/basic.lean
feat(logic/function): define `function.involutive` (#1474) …
Added function.involutive.to_equivView on Github →