Documentation

Mathlib.Control.EquivFunctor.Instances

EquivFunctor instances #

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

source
instance EquivFunctorUnique :
EquivFunctor Unique
Equations
    source
    instance EquivFunctorPerm :
    EquivFunctor Equiv.Perm
    Equations
      source
      instance EquivFunctorFinset :
      EquivFunctor Finset
      Equations
        source
        instance EquivFunctorFintype :
        EquivFunctor Fintype
        Equations