Documentation

Mathlib.Control.EquivFunctor.Instances

EquivFunctor instances #

We derive some EquivFunctor instances, to enable equiv_rw to rewrite under these functions.

source
@[implicit_reducible]
instance EquivFunctorUnique :
EquivFunctor Unique
source
@[implicit_reducible]
instance EquivFunctorPerm :
EquivFunctor Equiv.Perm
source
@[implicit_reducible]
instance EquivFunctorFinset :
EquivFunctor Finset
source
@[implicit_reducible]
instance EquivFunctorFintype :
EquivFunctor Fintype